#17098 
Add a search facility

PierreYves Strub

enhancement

4

Documentation

pre1.x

#17252 
The `seq` variant documented as pHL is in fact the HL tactic.

Alley Stoughton

defect

3

Documentation

pre1.x

#15506 
Issues when cloning theories

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15612 
require Theory issues misleading "added" messages

PierreYves Strub

defect

1

EasyCrypt

pre1.x

#15647 
Can't extract easily function from tuple

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15651 
lambda in operator doesn't work

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#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

#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

#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

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15786 
Swap with call to the adversary


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

#15813 
call tactic signals an "unknown symbol" error

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

#15827 
memory restriction for adversary does not take inner modules into account

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15841 
No explicit binding in equiv creates problems

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15842 
Bug in lambda translation

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15851 
[rnd] for map update produces confusing postconditions

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15871 
Stack Overflow

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15872 
fun stopped working

ckunz

defect

5

EasyCrypt

pre1.x

#15873 
Bug Printer

PierreYves Strub

defect

2

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

#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

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15893 
Call in adversary call is not working properly

Benjamin Grégoire

defect

4

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

#15916 
Extraneous internal memory identifier "hr" in output

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#15919 
[case] tactic for bd_hoare is useless

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15920 
[conseq (_ : pre => _)] tactic for bd_hoare doesn't work

Santiago ZanellaBéguelin

defect

3

EasyCrypt

pre1.x

#15924 
Assertion failed in otherwise provable goal

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15949 
Improve kill error message

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#15950 
tactics for fundamental lemma

Benjamin Grégoire

enhancement

4

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

#15974 
The following example generates an anomaly

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15980 
inconsistency due to choosing from empty distribution

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15981 
"delta cpEq" causes an untypable goal to be produced

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15982 
Printer bug for partially applied infix operators in prefix form

Benjamin Grégoire

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

#16000 
repeated instantiation and losslessness of 3argument fun don't work well together

Benjamin Grégoire

defect

3

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

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

PierreYves Strub

defect

2

EasyCrypt

pre1.x

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

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16104 
naming issues


enhancement

3

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

#16137 
universal elimination doesn't enforce { ... } restriction on module

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16138 
assertion failure when call tactic not given { ... } module restriction

Benjamin Grégoire

defect

3

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

#16174 
Bug in bdhoare call

ckunz

defect

3

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

#16228 
glob M computation problem with functors and inner modules for {*}

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16231 
General issues with computation of globals for nested modules

Benjamin Grégoire

defect

3

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

#16306 
Bug in cloning ?

Benjamin Grégoire

defect

5

EasyCrypt

pre1.x

#16362 
Assertion failure when cloning a theory with let expressions

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16399 
Bug in congr?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16416 
FEL completeness  initialization

Benjamin Grégoire

enhancement

3

EasyCrypt

pre1.x

#16457 
try tactic not catching case failure

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16468 
try fails to catch some callrelated exceptions


defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

2

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16648 
Make notations and tactics on distributions and functions a bit more uniform.


enhancement

3

EasyCrypt

pre1.x

#16656 
bug in parser with rewrite?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16692 
bug in apply.

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#16725 
Intro pattern for substitution

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16726 
Stack overflow during unification

PierreYves Strub

defect

3

EasyCrypt

pre1.x

(more results for this group on next page)
