#15612 
require Theory issues misleading "added" messages

PierreYves Strub

defect

1

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

1

EasyCrypt

pre1.x

#17071 
Error message for [expect]

<default>

enhancement

1

EasyCrypt

pre1.x

#17185 
Anomalies should give rise to a "This is a bug, please report."type message.

PierreYves Strub

enhancement

1

EasyCrypt

pre1.x

#17204 
Syntax for ignoring the return value of a procedure call

PierreYves Strub

enhancement

1

EasyCrypt

pre1.x

#17294 
`Self` (and `Top`) should be allowed in module restrictions

PierreYves Strub

defect

1

EasyCrypt

pre1.x

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

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#15873 
Bug Printer

PierreYves Strub

defect

2

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

#15949 
Improve kill error message

PierreYves Strub

enhancement

2

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

#16002 
bad error message when predicate is given polymorphic constant

PierreYves Strub

defect

2

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

#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

#16114 
Bad error message

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16117 
Fail to pose an arbitrary lambda

PierreYves Strub

defect

2

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

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

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16457 
try tactic not catching case failure

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

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

PierreYves Strub

defect

2

ProofGeneral

pre1.x

#16773 
"do! rewrite /op" loops

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17007 
Inconsistent syntax for closing sections/theories


enhancement

2

EasyCrypt

pre1.x

#17011 
Prettyprinter in adding too much scoping annotation

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17026 
EasyCrypt does not compile on Windows (win32 / cygwin)

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17049 
"restart scripting" not working in ProofGeneral


defect

2

ProofGeneral

pre1.x

#17074 
Option to destruct disjunctive hypotheses in [progress]

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#17093 
Add the possibility to declare several operators/predicates in 1 command.

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#17110 
[anomaly] on using [call] with a lemma referring to the wrong procedure

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17199 
PG: Default weakcheck mode indicator is invalid.

PierreYves Strub

defect

2

ProofGeneral

pre1.x

#17227 
Procedures with unit return type should be allowed to return `tt'

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#17249 
`AlgTactic` && `Ring` should agree on their axioms.

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#17266 
Clear goal window when no more goals

PierreYves Strub

enhancement

2

ProofGeneral

pre1.x

#17310 
Toplevel command to print various databases (exact, rewrite, ...)

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17369 
imprecise pretty printing with functor application


defect

2

EasyCrypt

pre1.x

#15506 
Issues when cloning theories

PierreYves Strub

defect

3

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

#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

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

PierreYves Strub

defect

3

ProofGeneral

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

#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

#15853 
timeout and prover settings are not undone

PierreYves Strub

defect

3

ProofGeneral

pre1.x

#15871 
Stack Overflow

PierreYves Strub

defect

3

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

#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

#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

#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

#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

#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

#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

#16115 
Subst failed

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16116 
rewrite /op failed with lambda

PierreYves Strub

defect

3

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

#16174 
Bug in bdhoare call

ckunz

defect

3

EasyCrypt

pre1.x

#16222 
Functor application circumvents sectionlocality

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

(more results for this group on next page)
