#15676 
Zeta tactics takes too much time to end(infinite loop ?)

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15702 
Error with multiple require if they contain the same game

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#15715 
Can't access a variable from a functor in probability formula

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15716 
Problem with introduction of Module in Proof

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15737 
Typesoundness issue when implementing module signatures

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15738 
Typing functor applications inside modules

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15742 
Strange error raised during a call to trivial

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15744 
require import causes name collisions in sub theories

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15762 
Tactic to transform a tuple equality into a conjonction

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15764 
Result not introduce after call in hoare logic

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15768 
Inlining with functor and cloning doesn't work

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15769 
ProofGeneral issue with new EasyCrypt: undo step at EOF give Emacs type error

PierreYves Strub

defect

3

ProofGeneral

pre1.x

#15779 
Inference during apply

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15781 
Bug into env insertion of a specific axiom Pr[]

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15791 
import doesn't import function from module

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15794 
Operator not found

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15808 
Declaring/defining mixfix operators, using them when not in scope

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15809 
Parsing/Printing scope for operator overloading "(x op y)%Scope"

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15813 
call tactic signals an "unknown symbol" error

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15814 
call tactic accepts variable defined in left game ({1}) defined for right game

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15815 
Search path for theories should include path of currently active file

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#15817 
Lighten EC syntax by removing the clumsy "<:" && "&" notations for modules / memories introductions / applications

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#15849 
Ignoring proof that are already done in a file

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15851 
[rnd] for map update produces confusing postconditions

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15852 
Undo immediately after 'save.' does not work

PierreYves Strub

defect

1

ProofGeneral

pre1.x

#15853 
timeout and prover settings are not undone

PierreYves Strub

defect

3

ProofGeneral

pre1.x

#15854 
Allow sequences of variable declarations in procedure definitions

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15859 
Omit path when it can be inferred from context

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15871 
Stack Overflow

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15873 
Bug Printer

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#15874 
Add support for chaining relations

PierreYves Strub

enhancement

1

EasyCrypt

pre1.x

#15877 
Apply is not working when trying to use it to instantiate a lemma that is quantified on modules

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15880 
Constant propagation with module variable

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15881 
Complete path for local variable in printer

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15882 
tuple and memory misprinted

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15884 
Repeat tactic broken

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15891 
Instantiating axioms and subtheories when cloning theories

PierreYves Strub

enhancement

4

EasyCrypt

pre1.x

#15892 
It should not be possible to close a theory where not all proofs are finished

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15906 
(local) opening of modules

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#15907 
clone import and clone export

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15908 
Unification variables appear

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15909 
firstlast tactical do not have the right precedence w.r.t tactics chaining (t1; t2)

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15910 
Wrong precedence for negation "!"

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#15912 
Be able to inline only one side after an equiv

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#15915 
conjunctive introduction pattern does not split <=>

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#15916 
Extraneous internal memory identifier "hr" in output

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#15917 
Proving "a = b => f a = f b" should not require a call to SMT

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15924 
Assertion failed in otherwise provable goal

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15930 
Clear all

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#15949 
Improve kill error message

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#15962 
Rewrite Fails because it didn't manage to infer type whereas it could

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15965 
Assertion failure in EcEnv

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15966 
Something wrong with installation script?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15970 
PG does not handle local lemmas properly.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15975 
Cfold bug with notation x.[a] =

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15990 
trivial cannot prove chained relations directly

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#15996 
rewriting when using intro patterns to eliminate existentials

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#15998 
Problem in cloning

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15999 
Pretty printer add too much scoping annotations.

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16001 
Instantiating an internal theory when cloning fails

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16002 
bad error message when predicate is given polymorphic constant

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16013 
Bug in theory realization

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16015 
lack of dot in map subscripting leads to assertion failure

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16054 
Bug in theory cloning with theory instanciation and export

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16055 
confusion of x{1} and x{2} with x in cut

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16066 
bad line number in error message when run in batch mode

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16067 
bad error message when value is treated as function

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16073 
Syntax to have ={} working for explicitly quantified memory

PierreYves Strub

enhancement

1

EasyCrypt

pre1.x

#16082 
move * for adversary function outside { ... }

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16086 
Missing error message: "Abstract function <function name> cannot be inlined."

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16087 
New view for apply: !a > (a => false)

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#16102 
bad error message when value of constant refers to module variable

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16111 
Strange bug in require

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16112 
Rnd on different type possible

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16114 
Bad error message

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16115 
Subst failed

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16116 
rewrite /op failed with lambda

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16117 
Fail to pose an arbitrary lambda

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16140 
Strange error in typing

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16141 
Not catched error in split

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16149 
printer bug: parentheses in types

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16150 
Multiple import

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16165 
"fixed" a breaking test case that may have been left as a TODO

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16222 
Functor application circumvents sectionlocality

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16226 
Some usages of the 'by' tactical do not discharge final trivial goals

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16264 
Bug in rewrite with let

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16288 
uncatched exception with functor inside functor

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16399 
Bug in congr?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16456 
allow expression, formula in cloning

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16457 
try tactic not catching case failure

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16459 
elim failing on patternmatching let expressions

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16460 
elim fails on let statements that can be simplified away

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16504 
Parse error on complex arguments to functions in probability statements

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16512 
Bug in pose

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16620 
Failure to patternmatch functional terms when they are applied in the goal.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16629 
cloning within sections

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16656 
bug in parser with rewrite?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16657 
Patternmatching on records

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16663 
Goal window should update on tactic failure...

PierreYves Strub

defect

2

ProofGeneral

pre1.x

#16691 
the name <top> should be accessible to the user.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

(more results for this group on next page)
