id,Summary,Owner,Type,Priority,Component,Version
17378,Proof of false using smt and Eprover.,Pierre-Yves Strub,defect,5,EasyCrypt,pre-1.x
17141,Wrong module type annotations accepted,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17024,Pattern matching should try to infer memory and module parameters,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17034,Generalizing loop fusion,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17040,Syntactic sugar for nested if-then-else statements.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17042,Pattern matching in non-normal form.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17070,better error message when difference between goal and lemma is tiny,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17195,Swap with 2 args move as far down as possible,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17250,off-by-one error in swap,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17309,`rewrite /F` when F is a fixpoint should simplify selected occurence for head-iota reduction.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17392,problems with glob and delta and matching,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17408,issue warning or error message when defining theory whose name clashes with one treated specially by EasyCrypt,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16113, in printer,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
17181,slow rewriting for large expressions,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17194,anomaly: EcHiGoal.LowApply.NoInstance (in byequiv),Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
17207,Applicative view,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17222,local clones do not disappear from the environment on section end,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17240,Syntactic sugar for proc. that reduces to a call to an external proc.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17255,Missing unification in `clone...with...`,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17256,apply/rewrite should work modulo zeta-reduction.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17261,`rewrite -/(f _)` should not match its own unfoldings.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17262,Add the possibility to add rewrite hints to rewrite hint databases.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17263,Multiple incompleteness in `apply`,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17265,`goal` vernacular command,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17268,Add a tactical that fails when no progress is done.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17271,Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn`,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17319,Anomaly triggered by `smt`,,defect,3,EasyCrypt,pre-1.x
17334,this message need more information: cannot infer all placeholders,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17335,the formula contains free type variables,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17402,Automatically package and publish up-to-date tutorial proofs,Pierre-Yves Strub,enhancement,3,Documentation,pre-1.x
17409,Termination checker failure,,defect,3,EasyCrypt,pre-1.x
17117,Warning when restrictions over an adversary are empty,Benjamin Grégoire,enhancement,2,EasyCrypt,pre-1.x
17160,Call SMT in parallels.,Pierre-Yves Strub,enhancement,2,Internals,pre-1.x
17253,EasyCrypt should fail gracefully when applying a tactic on a solved goal.,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
17264,Add the possibility to clear lemmas when closing a theory.,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
17347,Search with notations is broken.,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
17343,(Optional) warning for old syntax,Pierre-Yves Strub,enhancement,1,EasyCrypt,pre-1.x
17345,Bad printing,Pierre-Yves Strub,defect,1,EasyCrypt,pre-1.x
17364,Internals: use Batteries maps instead of Why3 ones.,Pierre-Yves Strub,enhancement,1,EasyCrypt,pre-1.x
15872,fun stopped working,ckunz,defect,5,EasyCrypt,pre-1.x
16306,Bug in cloning ?,Benjamin Grégoire,defect,5,EasyCrypt,pre-1.x
16787,new conseq issues,Benjamin Grégoire,defect,5,EasyCrypt,pre-1.x
17013,EasyCrypt toolchain does not compile anymore on OSX,Pierre-Yves Strub,defect,5,EasyCrypt,pre-1.x
17027,[Unsoundness] The HL and pHL tactics for abstract function calls do not quantify over variables that may be modified in the postcondition,Pierre-Yves Strub,defect,5,EasyCrypt,pre-1.x
17068,Possible bug in the union-find algorithm,Pierre-Yves Strub,defect,5,EasyCrypt,pre-1.x
17079,Make the test-suite pass.,Pierre-Yves Strub,defect,5,Libraries,pre-1.x
17109,Hoare adversary rule introducess references to non-existent memories in postconditions,Benjamin Grégoire,defect,5,EasyCrypt,pre-1.x
17112,`unknown symbol Top.o` when importing a theory including objects referring to `Top.o`,Pierre-Yves Strub,defect,5,EasyCrypt,pre-1.x
17114,Unsoundness of module system,Benjamin Grégoire,defect,5,EasyCrypt,pre-1.x
17132,"Unsoundness in definition of ""glob M""",Pierre-Yves Strub,defect,5,EasyCrypt,pre-1.x
17270,`done` should close a goal when `false` is a local hyp.,Pierre-Yves Strub,enhancement,5,EasyCrypt,pre-1.x
17365,Proof of false using Ring and Reals.,Pierre-Yves Strub,defect,5,EasyCrypt,pre-1.x
17379,Proving unreasonable/false lemmas through Alt-Ergo,,defect,5,EasyCrypt,pre-1.x
17380,"Internal ""seq"" of pHL tactics is unsound",Benjamin Grégoire,defect,5,EasyCrypt,pre-1.x
15702,Error with multiple require if they contain the same game,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
15891,Instantiating axioms and sub-theories when cloning theories,Pierre-Yves Strub,enhancement,4,EasyCrypt,pre-1.x
15893,Call in adversary call is not working properly,Benjamin Grégoire,defect,4,EasyCrypt,pre-1.x
15950,tactics for fundamental lemma,Benjamin Grégoire,enhancement,4,EasyCrypt,pre-1.x
16692,bug in apply.,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17012,pr_false is badly implemented (unsoundness),Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17035,Alt-Ergo succeeds on false obligations in weird circumstances,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17080,`t_generalize_hyps` does not work when given a non-singleton list.,Pierre-Yves Strub,defect,4,Internals,pre-1.x
17082,SMT tactic should be interruptable.,Pierre-Yves Strub,enhancement,4,EasyCrypt,pre-1.x
17087,[conseq*] should be the default behaviour of [conseq],Pierre-Yves Strub,enhancement,4,EasyCrypt,pre-1.x
17089,anomaly in [sim],Benjamin Grégoire,defect,4,EasyCrypt,pre-1.x
17098,Add a search facility,Pierre-Yves Strub,enhancement,4,Documentation,pre-1.x
17120,[rnd] allows to prove false,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17127,Bug in typing of instruction x.[y] = e;,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17148,Operators should be subject to section restrictions,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17155,Fix stdlib w.r.t. why3 import,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17162,Bad interaction between abstract theories and local modules,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17329,EasyCrypt output (goals order e.g.) is not stable,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
17339,`anomaly: EcLowGoal.InvalidProofTerm.` on `/>`,Pierre-Yves Strub,defect,4,EasyCrypt,pre-1.x
15502,"""Ident _[...] is not yet declared"" when cloning a theory with operators",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15506,Issues when cloning theories,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15520,request for more loop manipulation tactics,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15647,Can't extract easily function from tuple,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15651,lambda in operator doesn't work,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15676,Zeta tactics takes too much time to end(infinite loop ?),Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15715,Can't access a variable from a functor in probability formula,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15716,Problem with introduction of Module in Proof,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15737,Type-soundness issue when implementing module signatures,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15738,Typing functor applications inside modules,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15742,Strange error raised during a call to trivial,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15744,require import causes name collisions in sub theories,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15762,Tactic to transform a tuple equality into a conjonction,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15764,Result not introduce after call in hoare logic,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15768,Inlining with functor and cloning doesn't work,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15769,ProofGeneral issue with new EasyCrypt: undo step at EOF give Emacs type error,Pierre-Yves Strub,defect,3,ProofGeneral,pre-1.x
15779,Inference during apply,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15781,Bug into env insertion of a specific axiom Pr[],Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15786,Swap with call to the adversary,,defect,3,EasyCrypt,pre-1.x
15791,import doesn't import function from module,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15794,Operator not found,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15808,"Declaring/defining mixfix operators, using them when not in scope",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15809,"Parsing/Printing scope for operator overloading ""(x op y)%Scope""",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15813,"call tactic signals an ""unknown symbol"" error",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15814,call tactic accepts variable defined in left game ({1}) defined for right game,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15827,memory restriction for adversary does not take inner modules into account,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
15841,No explicit binding in equiv creates problems,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
15842,Bug in lambda translation,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
15849,Ignoring proof that are already done in a file,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15851,[rnd] for map update produces confusing post-conditions,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15853,timeout and prover settings are not undone,Pierre-Yves Strub,defect,3,ProofGeneral,pre-1.x
15854,Allow sequences of variable declarations in procedure definitions,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15859,Omit path when it can be inferred from context,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15871,Stack Overflow,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15877,Apply is not working when trying to use it to instantiate a lemma that is quantified on modules,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15879,While one sided,ckunz,enhancement,3,EasyCrypt,pre-1.x
15880,Constant propagation with module variable,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15881,Complete path for local variable in printer,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15882,tuple and memory misprinted,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15884,Repeat tactic broken,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15892,It should not be possible to close a theory where not all proofs are finished,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15907,clone import and clone export,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15908,Unification variables appear,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15909,first|last tactical do not have the right precedence w.r.t tactics chaining (t1; t2),Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15917,"Proving ""a = b => f a = f b"" should not require a call to SMT",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
15918,Tactic for proving an equiv/hoare/bd_hoare goal when the pre-condition is contradictory,Santiago Zanella-Béguelin,enhancement,3,EasyCrypt,pre-1.x
15919,[case] tactic for bd_hoare is useless,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
15920,[conseq (_ : pre => _)] tactic for bd_hoare doesn't work,Santiago Zanella-Béguelin,defect,3,EasyCrypt,pre-1.x
15921,"A strongest post-condition tactic [sp n m], like in trunk",ckunz,enhancement,3,EasyCrypt,pre-1.x
15922,if tactic for bd_hoare doesn't work with precondition true,Santiago Zanella-Béguelin,defect,3,EasyCrypt,pre-1.x
15924,Assertion failed in otherwise provable goal,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15962,Rewrite Fails because it didn't manage to infer type whereas it could,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15965,Assertion failure in EcEnv,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15966,Something wrong with installation script?,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15968,assertion failure when fun tactic for abstract function isn't given argument,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
15970,PG does not handle local lemmas properly.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15974,The following example generates an anomaly,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
15975,Cfold bug with notation x.[a] =,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15980,inconsistency due to choosing from empty distribution,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
15981,"""delta cpEq"" causes an untypable goal to be produced",Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
15982,Printer bug for partially applied infix operators in prefix form,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
15998,Problem in cloning,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16000,repeated instantiation and losslessness of 3-argument fun don't work well together,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16001,Instantiating an internal theory when cloning fails,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16013,Bug in theory realization,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16015,lack of dot in map subscripting leads to assertion failure,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16054,Bug in theory cloning with theory instanciation and export,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16055,confusion of x{1} and x{2} with x in cut,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16058,Syntax f.x in equiv precondition for fonction argument,,enhancement,3,EasyCrypt,pre-1.x
16082,move * for adversary function outside { ... },Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16104,naming issues,,enhancement,3,EasyCrypt,pre-1.x
16111,Strange bug in require,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16112,Rnd on different type possible,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16115,Subst failed,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16116,rewrite /op failed with lambda,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16137,universal elimination doesn't enforce { ... } restriction on module,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16138,assertion failure when call tactic not given { ... } module restriction,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16140,Strange error in typing,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16141,Not catched error in split,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16149,printer bug: parentheses in types,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16174,Bug in bdhoare call,ckunz,defect,3,EasyCrypt,pre-1.x
16222,Functor application circumvents section-locality,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16228,glob M computation problem with functors and inner modules for {*},Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16229,Substitution issue when quantified module variables have the same name as an existing module,,defect,3,EasyCrypt,pre-1.x
16231,General issues with computation of globals for nested modules,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16253,Non-local modules and abstract restrictions.,,defect,3,EasyCrypt,pre-1.x
16264,Bug in rewrite with let,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16288,uncatched exception with functor inside functor,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16292,Side-conditions for the rnd rule in pHL should be proved under some precondition,ckunz,defect,3,EasyCrypt,pre-1.x
16362,Assertion failure when cloning a theory with let expressions,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16399,Bug in congr?,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16416,FEL completeness - initialization,Benjamin Grégoire,enhancement,3,EasyCrypt,pre-1.x
16456,"allow expression, formula in cloning ",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16468,try fails to catch some call-related exceptions,,defect,3,EasyCrypt,pre-1.x
16512,Bug in pose,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16560,Non-relational 'bypr' for probabilistic Hoare statements,ckunz,enhancement,3,EasyCrypt,pre-1.x
16620,Failure to pattern-match functional terms when they are applied in the goal.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16628,making nested sections work,,enhancement,3,EasyCrypt,pre-1.x
16629,cloning within sections,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16648,Make notations and tactics on distributions and functions a bit more uniform.,,enhancement,3,EasyCrypt,pre-1.x
16656,bug in parser with rewrite?,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16657,Pattern-matching on records,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16691,the name should be accessible to the user.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16723,Subtyping for abstract modules and functors,Benjamin Grégoire,enhancement,3,EasyCrypt,pre-1.x
16725,Intro pattern for substitution,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16726,Stack overflow during unification,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16727,"bd_hoare should work on >=, rather than forcing us to swap arguments",Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16729,Tactic swap causes inconsistent dependencies,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16732,Problem with functor aliases when outermost module is a parameter,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16737,"""declare op""",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16749,link between hoare bdhoare equiv,Benjamin Grégoire,enhancement,3,EasyCrypt,pre-1.x
16751,hoare should work on fun.,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16763,Simplification should discriminate datatype constructors,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16772,Weird error with inductives when aliasing constructors,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16775,EasyCrypt insists on typing boolean-returning fixpoints as predicates,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16780,Change the test script so the test suites can be run in weak check mode,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16786,Nicer treatment of datatype constructors,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16788,Another stack overflow during unification,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16789,Pattern matching should to some top-level delta-unfolding,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16790,Bug when cloning and instantiating an abstract type,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16811,inline * should not try to inline abstract function,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16840,"@ can be used to define infix operators, but cannot be used to apply them",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16849,Broken proc (in branch 1.0),Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16856,Blocker typing bug in rnd (master),Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16918,"selection tactical ""all n""",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16963,op/pred nosmt ...,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16964,Warn when a variable is used before being initialized,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
16965,Non-termination when expanding a procedure whose body contains a generic projector (.`n),Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
16966,Many lexer errors related to the universal projector notation (.'n),Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16983,equiv generates ill-typed formulas on ill-typed input (instead of an error),Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16984,Anomaly due to inlining functions with tuple arguments,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
16986,"""while >="" generates invalid goals",ckunz,defect,3,EasyCrypt,pre-1.x
16990,Generalization does not cross tuple projections.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17005,Higher-order pattern matching,,enhancement,3,EasyCrypt,pre-1.x
17006,Instantiating an abstract procedure taking n-uple with a n-ary concrete procedure,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17009,1.x error messages,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17016,Make elim and case work on tuples and records. Retire the special lemmas,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17018,splitwhile syntax is still weird,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17021,Some judgment-combining variants of conseq do not apply to procedures,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
17033,Some program logic tactics that modify the precondition use bad associativity,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17038,Message with anomaly,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17044,Bad inlining when giving an argument of type unit to a procedure that expects no arguments,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17046,possible tactic renaming: [proc *] -> [eager proc *],Benjamin Grégoire,enhancement,3,EasyCrypt,pre-1.x
17047,"pretty printing of module type uses old notation for ""*""",,defect,3,EasyCrypt,pre-1.x
17050,elim/let anomaly,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17051,Pretty-printing regression,,defect,3,EasyCrypt,pre-1.x
17052,Parse error on (**),Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17053,Bogus goal when variable shadows a module,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17054,Finiteness of product of finite types,,enhancement,3,Libraries,pre-1.x
17055,Lemma linking eq_except and in_dom in FMap,,enhancement,3,Libraries,pre-1.x
17057,Add the possibility to rule out the prover filtering mecanism from the command line.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17059,Negative line selectors in program logic tactics,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17060,"pretty printer still using ""lambda"" instead of ""fun""",,defect,3,EasyCrypt,pre-1.x
17061,"when arguments to seq are too big, anomaly rather than error message",,defect,3,EasyCrypt,pre-1.x
17065,Invalid priority of `by` w.r.t `;`,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17066,Better error message when operator selection failed.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17067,Syntax for chained case analysis of the top-assumption,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17069,Improve error messages of the (P?R)HL tactics,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17072,Pretty Printer Glitches for !(_ = _),Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17073,`case` intro-pattern does not try to head-reduce if the goal is not subject to intro.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17075,[sp] should fail when given code positions that cannot be reached,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17078,EasyCrypt should use big integers internally.,Pierre-Yves Strub,defect,3,Internals,pre-1.x
17083,Missing eta-reduction in conversion,Benjamin Grégoire,enhancement,3,EasyCrypt,pre-1.x
17084,syntax for non-flat proof-terms,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17091,[rewrite] should head-reduce created b-redexes,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17092,Chaining [apply],Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17094,Refactoring: code for operators addition.,Pierre-Yves Strub,enhancement,3,Internals,pre-1.x
17095,anomaly raised by invariant form of [call upto],,defect,3,EasyCrypt,pre-1.x
17096,Unfolding should work even in the presence of several matching operators.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17097,Bad pretty-printing of lists.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17099,Forward `apply` should be accessible for the top-assumption in intro-patterns,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17100,Forward `apply` should be accessible for the top-assumption in intro-patterns,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17101,[anomaly] when defining an operator over a concrete module's globals,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17102,[anomaly] when pHL => pRHL variant of conseq is used with a bound different from [=1%r],Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17106,Unification should work modulo delta-unfolding / simplification.,,enhancement,3,EasyCrypt,pre-1.x
17107,"Potential mismatch between spec and lemma versions of the ""pHL + HL => pHL"" variant of [conseq]",,defect,3,EasyCrypt,pre-1.x
17108,require clone,,enhancement,3,EasyCrypt,pre-1.x
17115,[exfalso] tactic for ambient logic,,enhancement,3,EasyCrypt,pre-1.x
17116,Bad error message for [swap],Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17118,Add the ability to print the axioms of the environment,,enhancement,3,EasyCrypt,pre-1.x
17119,Give the ability to print subgoals,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17121,Make Option.witness accessible at top level,,enhancement,3,EasyCrypt,pre-1.x
17122,Clone ignores provided proof,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17123,"Bad parsing on call (_: B, I)",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17124,allows to specify timeout only for smt.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17125,Cannot clear variables referring to memory,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17126,Command and command line option for global timeout multiplier.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17128,assert false in rnd.,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
17129,"bug in alias, the introduced variable has not the good type.",Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
17130,"""alias i"" works only on random instruction.",Benjamin Grégoire,enhancement,3,EasyCrypt,pre-1.x
17133,seq for phoare do not check the type of the arguments.,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
17134,is_lossless F(M).f generate a parse error.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17135,anomaly when intro pattern has wrong form,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17136,variant of seq to deal with large preconditions,,enhancement,3,EasyCrypt,pre-1.x
17137,More tactical about goal selections,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17138,"""easycrypt -check-all"" does not load ""Logic""",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17139,Multiple require at once.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17142,Anomaly (related to SMT and memories),Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
17143,Anomaly (free type variables in conseq),Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17144,Module type checking: Unclear error message and probably bug,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17145,"""choice"" reorders its arguments",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17146,Bad error message in combination choice/modules/section,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17147,Parse error in (some) expressions involving memories,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17151,Abstract theories,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17153,seq does not check type of its arguments,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17154,anomaly: EcPV.MemoryClash,,defect,3,EasyCrypt,pre-1.x
17158,"""<-"" for predicates when cloning",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17159,expect should support goal selection,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17165,not-to-be-proved lemmas,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17166,"missing syntax for proving all axioms of a theory, its subtheories, etc., when cloning",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17167,Better localization of errors when typing a proof-term,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17168,"Unsoundness: combination of sections, modules, and choice-operators",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17170,Introduce theory for product distribution,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17171,mode similar to nocheck that tries smt calls and just prints the locations for the failing calls,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17172,Looping on `rewrite !/op`,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17173,"alternative to ""require A; clone export A as B"" that does not add A to SMT context",,enhancement,3,EasyCrypt,pre-1.x
17174,Return of the memory explosion,,defect,3,EasyCrypt,pre-1.x
17176,[print] should display types even on fixpoints,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17177,View application fails non gracely when it cannot instanciate all type variables.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17178,Generalizing over an empty list should generate a sane name,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17179,`done` should close goals with a direct contradiction in its env.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17180,"anomaly: File ""src/ecCoreFol.ml"", line 1207, characters 19-25: Assertion failed",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17184,parse error involving parameterized module,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17187,anomaly when invalid memory is referenced -- should be proper error message,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17188,Error with smt : lazy,,defect,3,EasyCrypt,pre-1.x
17189,Syntax for referring to *local* variables by their long name,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17190,progress and progress => //. should be equivalent...,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17191,Assert failure,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17193,Obscure failure on lazy smt with higher-order stuff and booleans,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17196,Vernacular command for dumping env. as a Why3 task.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17198,Spurious failure of rewrite,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17200,Parse error in required theories are incorrectly located.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17201,`x-y` and `x + -y` should be convertible,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17203,Rewrite strangely failling,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17205,New syntax for assignments should be available in immediate definitions,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17206,Missing parens in the pretty printer,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17208,`rewrite ... in ...`,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17211,split causes anomaly when given equality between constructors,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17212,Circular [require] dependencies should be caught instead of blowing up computers,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17213,Retracting/Resetting should cause easycrypt to reload the prelude,Pierre-Yves Strub,defect,3,ProofGeneral,pre-1.x
17214,Wrong printed for memory,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17216,All test suites should include abstract theory files (*.eca),,defect,3,Internals,pre-1.x
17219,operators don't print the way they are declared,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17220,"Shorthand ""by"" syntax should be supported for ""realize""",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17221,parsing change allowing lemma ... by tactics,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17223,use of ' and ` in operator names causes anomaly rather than error message,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17224,type declarations with bad type variables yield anomalies rather than error messages,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17226,some weirdness with operators of form :+,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17228,pretty printer uses bad syntax for type constructors,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17229,pretty printer errors with inductive datatypes,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17230,unhelpful error message when there are two matching operators with needed type,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17231,"check for datatype being inhabited isn't complete, but error message suggests it is",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17232,weirdness involving redefining (=) or defining (<>),,enhancement,3,EasyCrypt,pre-1.x
17233,pretty printing issues with _?_:_ and modules,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17234,Allow omission of a procedure's return type when it can be inferred,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17235,rewrite ... in ... should allow rewriting in uident not just lident,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17236,error with rewriting occurrence of -1 when only one matching occurrence,,defect,3,EasyCrypt,pre-1.x
17237,failure of rewrite ... in ...,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17238,anomaly with auto-revert intro pattern,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17241,`clone import` not working when realizing axioms.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17242,`print` should display `nosmt` info,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17243,Internal error (anomaly) on proof script,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17244,"Imprecise ""uninitialized local variables"" warning",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17247,Interactive proof realisation for `instance`,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17248,More precise error messages when non-interactive realization fails,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17252,The `seq` variant documented as pHL is in fact the HL tactic.,Alley Stoughton,defect,3,Documentation,pre-1.x
17254,print produces misleading results on partially applied functors,,defect,3,EasyCrypt,pre-1.x
17258,Intro pattern for hypothesis duplication,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17260,pragma +option should fail gracefully.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17269,Add notations for >/>=,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17272,Wrong name,,defect,3,EasyCrypt,pre-1.x
17273,`alias` failures look like uncaught exceptions,,defect,3,EasyCrypt,pre-1.x
17274,"Collision in names, local variables unreachable",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17275,[congr] should apply to iff,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17276,the pretty printer is getting the relative precedences of unary - and %% wrong,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17277,Higher-order pattern-matching with quantifiers,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17278,[eta] reduction is not full on multi-ary functions,github ,defect,3,EasyCrypt,pre-1.x
17280,Parse-only abbreviations,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17284,Support for `={}` in equiv contracts,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17289,Missing dependencies in OPAM package,,defect,3,EasyCrypt,pre-1.x
17290,`n!->>` should work,,enhancement,3,EasyCrypt,pre-1.x
17291,`move: x` should keep the body of `x` if any.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17292,anomaly on application of a `<=>` lemma to a `=` goal,,defect,3,EasyCrypt,pre-1.x
17293,Looping behaviour in reduction/simplification. Probably related to reals.,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17296,Some program tactics (`rnd`) generate invalid formulas when Distr is not loaded,,defect,3,EasyCrypt,pre-1.x
17299,Transitivity using an equiv,,enhancement,3,EasyCrypt,phl
17300,Module type checks have wrong variance when dealing with some functor configurations,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
17302,fel can generate subgoal with undefined memory,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
17303,more fel peculiarities,Benjamin Grégoire,defect,3,EasyCrypt,pre-1.x
17304,Regression on anonymous procedure arguments support,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17306,Operator folding and unfolding not checking type parameters,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17308,"`rewrite !(A,B)` loops when `B` is not known about",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17312,cloning can create ill-formed definitions,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17313,module types with multiple occurrences of same procedure should not be accepted,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17314,Syntax variants of multiple argument module types don't match ones for parameterized modules,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17315,[print] on notations is not very useful,,defect,3,EasyCrypt,pre-1.x
17317,`search` should work somewhat better with abbreviations,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17318,clone-time regexp substitution should apply in the specified order,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17320,anomaly when cloning theory with inductive predicate,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17321,`case @[ambient]` needs its syntax unified with that of ambient `case`,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17323,|> ip anomaly,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17324,|> ip expands predicates in conclusion,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17326,`+` intro-pattern may reorder assumptions,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17327,Variants of `<*>` with preference,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17328,`_` intro-pattern should only check if the clear is possible once the rest of the intro-pattern has been processed,,enhancement,3,EasyCrypt,pre-1.x
17330,anomaly on `apply/contra`,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17331,Tactic arguments for the `exists` tactic should not be comma-separated,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17332,Better localisation when a pattern cannot be infered,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17333,We need a `pragma` to stop EasyCrypt from reducing `b => false` into `!b`.,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17336,`inline` procedure selection by code position,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17338,misspelled pragmas are not reported,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17348,Intro-pattern `|>` might transform a provable goal to a non-provable one,,defect,3,EasyCrypt,pre-1.x
17350,witness not in apRHL,,defect,3,EasyCrypt,pre-1.x
17352,Question about run easycrypt,,task,3,EasyCrypt,pre-1.x
17354,"In cloning, `rename` should not be allowed to create unreachable/unparsable symbols",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17355,Pretty-printer sometimes forget to use the abbreviation,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17359,`rewrite ?lem` should fail (hard) if `lem` does not exist in scope,,enhancement,3,EasyCrypt,pre-1.x
17361,scoping problem with theory renaming,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17362,wildcard syntax for SMT provers in prover [...],,enhancement,3,EasyCrypt,pre-1.x
17366,crush losing some context on intermediate substitutions,,defect,3,EasyCrypt,pre-1.x
17371,new option for smt,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17372,""""" and ""!"" semantic for smt",Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17373,introduction pattern bug somehow related to SmtMap,,defect,3,EasyCrypt,pre-1.x
17375,`include` command for modules / module types,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17376,behaviour of module type include in functor types,Benjamin Grégoire,enhancement,3,EasyCrypt,pre-1.x
17377,characterization lemmas for <=> and \proper,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17385,problem sending goal to SMT (involving inductive datatype and higher order function),Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17386,crush reduces goal whose conclusion is `y1 = y2 <=> x1 = x2` to false goal,,defect,3,EasyCrypt,pre-1.x
17387,no error message for match,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17389,inline does not inline under match statement,,defect,3,EasyCrypt,pre-1.x
17391,"case works with tuple corresponding to glob M, but not with glob M",Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17393,Cloning polymorphic datatypes does not allow case analysis,,defect,3,EasyCrypt,pre-1.x
17394,anomaly on some smt calls,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17397,odd scoping when overwriting operator in theory cloning,,enhancement,3,EasyCrypt,pre-1.x
17398,problem with new eco facility,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17400,eco problem: .ec file that uses unchanged .ec file is rechecked even though nothing changed and eco files stable,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
17401,Generalizations may perform freeness checks in the wrong context,,defect,3,EasyCrypt,pre-1.x
17403,Support for `move/(_ _ x): H=> H`,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17411,unexpected behavior from crush?,,defect,3,EasyCrypt,pre-1.x
17412,commit b1b35e64ac8878bd0b564659d0582378a8c23204 broke module simple definition,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x
15106,Consider probability quantities as real-valued expressions,,enhancement,2,EasyCrypt,pre-1.x
15815,Search path for theories should include path of currently active file,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
15817,"Lighten EC syntax by removing the clumsy ""<:"" && ""&"" notations for modules / memories introductions / applications",Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
15873,Bug Printer,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
15906,(local) opening of modules,Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
15910,"Wrong precedence for negation ""!""",Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
15912,Be able to inline only one side after an equiv,Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
15915,conjunctive introduction pattern does not split <=>,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
15916,"Extraneous internal memory identifier ""hr"" in output",Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
15930,Clear all,Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
15949,Improve kill error message,Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
15990,trivial cannot prove chained relations directly,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
15996,rewriting when using intro patterns to eliminate existentials,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
15999,Pretty printer add too much scoping annotations.,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16002,bad error message when predicate is given polymorphic constant,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16066,bad line number in error message when run in batch mode,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16067,bad error message when value is treated as function,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16086,"Missing error message: ""Abstract function cannot be inlined.""",Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16087,New view for apply: !a -> (a => false),Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
16102,bad error message when value of constant refers to module variable,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16114,Bad error message,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16117,Fail to pose an arbitrary lambda,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16150,Multiple import,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16165,"""fixed"" a breaking test case that may have been left as a TODO",Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16226,Some usages of the 'by' tactical do not discharge final trivial goals,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16457,try tactic not catching case failure,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16459,elim failing on pattern-matching let expressions,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16460,elim fails on let statements that can be simplified away,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16504,Parse error on complex arguments to functions in probability statements,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
16622,"Functor-level ""lambdas""",Benjamin Grégoire,enhancement,2,EasyCrypt,pre-1.x
16663,Goal window should update on tactic failure...,Pierre-Yves Strub,defect,2,ProofGeneral,pre-1.x
16746,Losslessness annotations,Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
16773,"""do! rewrite /op"" loops",Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
17007,Inconsistent syntax for closing sections/theories,,enhancement,2,EasyCrypt,pre-1.x
17011,Pretty-printer in adding too much scoping annotation,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
17026,EasyCrypt does not compile on Windows (win32 / cygwin),Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
17049,"""restart scripting"" not working in ProofGeneral",,defect,2,ProofGeneral,pre-1.x
17074,Option to destruct disjunctive hypotheses in [progress],Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
17093,Add the possibility to declare several operators/predicates in 1 command.,Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
17110,[anomaly] on using [call] with a lemma referring to the wrong procedure,Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
17199,PG: Default weak-check mode indicator is invalid.,Pierre-Yves Strub,defect,2,ProofGeneral,pre-1.x
17227,Procedures with unit return type should be allowed to return `tt',Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
17249,`AlgTactic` && `Ring` should agree on their axioms.,Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
17266,Clear goal window when no more goals,Pierre-Yves Strub,enhancement,2,ProofGeneral,pre-1.x
17310,"Top-level command to print various databases (exact, rewrite, ...)",Pierre-Yves Strub,defect,2,EasyCrypt,pre-1.x
17369,imprecise pretty printing with functor application,,defect,2,EasyCrypt,pre-1.x
17381,Possible bug: no matching operator even when available,,defect,2,EasyCrypt,pre-1.x
15612,"require Theory issues misleading ""added"" messages",Pierre-Yves Strub,defect,1,EasyCrypt,pre-1.x
15852,Undo immediately after 'save.' does not work,Pierre-Yves Strub,defect,1,ProofGeneral,pre-1.x
15874,Add support for chaining relations,Pierre-Yves Strub,enhancement,1,EasyCrypt,pre-1.x
16073,Syntax to have ={} working for explicitly quantified memory,Pierre-Yves Strub,enhancement,1,EasyCrypt,pre-1.x
16374,Visual weak-check indicator,,enhancement,1,ProofGeneral,pre-1.x
16885,Support for type annotations in let expressions,Pierre-Yves Strub,enhancement,1,EasyCrypt,pre-1.x
17071,Error message for [expect],,enhancement,1,EasyCrypt,pre-1.x
17104,Make (<>) accessible in prefix form,,enhancement,1,EasyCrypt,pre-1.x
17185,"Anomalies should give rise to a ""This is a bug, please report.""-type message.",Pierre-Yves Strub,enhancement,1,EasyCrypt,pre-1.x
17204,Syntax for ignoring the return value of a procedure call,Pierre-Yves Strub,enhancement,1,EasyCrypt,pre-1.x
17294,`Self` (and `Top`) should be allowed in module restrictions,Pierre-Yves Strub,defect,1,EasyCrypt,pre-1.x
17257,`/=` is too weak.,,defect,5,EasyCrypt,pre-1.x
17077,No more direct access to stdlib paths,Pierre-Yves Strub,defect,4,Internals,pre-1.x
17163,Check that `phoare` tactics are forcing the input bounds to be in [0..1].,,task,4,EasyCrypt,pre-1.x
17298,Super rnd,,enhancement,4,EasyCrypt,phl
16103,scoping issue with theories,,enhancement,3,EasyCrypt,pre-1.x
16987,Move facts from precondition to context,,enhancement,3,EasyCrypt,pre-1.x
17002,Better section && cloning support,Pierre-Yves Strub,task,3,EasyCrypt,pre-1.x
17022,Pattern-matching on variables in judgments and probability expressions,,enhancement,3,EasyCrypt,pre-1.x
17085,Generic Notations,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17086,Generalize [rewrite Pr],,enhancement,3,EasyCrypt,pre-1.x
17105,[transitivity] for phoare and hoare,,enhancement,3,EasyCrypt,pre-1.x
17113,Decide what to do on rewrite with defined head symbols,,enhancement,3,EasyCrypt,pre-1.x
17140,Pattern matching should make use of simplification rules.,,enhancement,3,EasyCrypt,pre-1.x
17149,Expand glob A for concrete module,,enhancement,3,EasyCrypt,pre-1.x
17156,New vernacular command: `print axiom`,,enhancement,3,EasyCrypt,pre-1.x
17164,behavior of -check-all,,enhancement,3,EasyCrypt,pre-1.x
17169,Anonymous functor arguments: passing procedures to functors directly,,enhancement,3,EasyCrypt,pre-1.x
17175,Direct intro on negative goals,,enhancement,3,EasyCrypt,pre-1.x
17192,Problem with `glob` and type inference,,defect,3,EasyCrypt,pre-1.x
17197,Asserts in equivalence proofs,,enhancement,3,EasyCrypt,pre-1.x
17202,Add seq* tactic,,enhancement,3,EasyCrypt,pre-1.x
17210,Pattern-matching for pairs in operator arguments,,enhancement,3,EasyCrypt,pre-1.x
17215,Issues with module typing when functor parameters are themselves functors,,defect,3,EasyCrypt,pre-1.x
17217,need better error message when attempting to apply lemma to goal that isn't a judgment,,enhancement,3,EasyCrypt,pre-1.x
17218,proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate,,enhancement,3,EasyCrypt,pre-1.x
17225,Explore reproducible smt calls,,enhancement,3,EasyCrypt,pre-1.x
17239,Mutual inductive types.,,enhancement,3,EasyCrypt,pre-1.x
17245,Formula manipulation commands (for `conseq` and `seq`),,enhancement,3,EasyCrypt,pre-1.x
17246,"`rewrite`, apply, ... in contracts",,defect,3,EasyCrypt,pre-1.x
17251,print Self,,enhancement,3,EasyCrypt,pre-1.x
17259,Theory of distribution (iso)morphisms,,task,3,Libraries,pre-1.x
17267,`auto` with `call`,,enhancement,3,EasyCrypt,pre-1.x
17279,Improve `invalid goal shape` error messages for variants of `byequiv`,,enhancement,3,EasyCrypt,pre-1.x
17281,Several problems with `apply` in program logics,,enhancement,3,EasyCrypt,pre-1.x
17282,call should not work,,task,3,EasyCrypt,phl
17283,pattern matching complexity problem,,defect,3,EasyCrypt,pre-1.x
17285,Transitivity on procedures should support inferring contracts from `equiv` lemmas.,,enhancement,3,EasyCrypt,pre-1.x
17286,pRHL `apply` should have a framing variant,,enhancement,3,EasyCrypt,pre-1.x
17287,Program transformation tactics should not `anomaly` without a side in pRHL,,defect,3,EasyCrypt,pre-1.x
17288,EasyCrypt crashes when printing required abstract theory IterProc,,defect,3,EasyCrypt,pre-1.x
17295,local ops,,enhancement,3,EasyCrypt,pre-1.x
17301,Applicative view for `if then else`,,enhancement,3,EasyCrypt,pre-1.x
17305,proc* in eager case needlessly assigns result of procedures returning unit to variables,,enhancement,3,EasyCrypt,pre-1.x
17311,`smt (@Self)`,,enhancement,3,EasyCrypt,pre-1.x
17316,[smt (@Theory)] should force the use of axioms marked as `nosmt`,,defect,3,EasyCrypt,pre-1.x
17322,use of side with HL version of while tactic should be syntax error,,defect,3,EasyCrypt,pre-1.x
17325,syntax marking end of cloning realization,,enhancement,3,EasyCrypt,pre-1.x
17337,substitutions should complain when substituting a locally defined variable,,enhancement,3,EasyCrypt,pre-1.x
17340,cfold should support variables (and more general terms).,,enhancement,3,EasyCrypt,pre-1.x
17341,for loops,,enhancement,3,EasyCrypt,pre-1.x
17342,Better support for rewriting with equivalences,,enhancement,3,EasyCrypt,pre-1.x
17344,Trees and polynomials,,enhancement,3,EasyCrypt,pre-1.x
17346,have access to notation in ml,,enhancement,3,EasyCrypt,pre-1.x
17349,call tactic for aequiv conclusions,,enhancement,3,EasyCrypt,pre-1.x
17351,sp for aqeuiv goals,,enhancement,3,EasyCrypt,pre-1.x
17357,rnd tactic for aprhl,,enhancement,3,EasyCrypt,pre-1.x
17358,A normalization operator,,enhancement,3,EasyCrypt,pre-1.x
17363,Conseq: do not how to combine equivF and hoareS and hoareS into equivS,,enhancement,3,EasyCrypt,pre-1.x
17367,abbreviations involving modules and memories,,enhancement,3,EasyCrypt,pre-1.x
17368,atomic formula of ambient logic expressing disjoint globals of modules,,enhancement,3,EasyCrypt,pre-1.x
17370,checking memory initialisation constraints,,enhancement,3,EasyCrypt,pre-1.x
17374,pre-/post- should be implemented with an explicit memory,,enhancement,3,Internals,pre-1.x
17382,glob M should reduce to a record,,enhancement,3,EasyCrypt,pre-1.x
17383,abstract operators in section should be generalized,,enhancement,3,EasyCrypt,pre-1.x
17384,module parametrised by expressions,,enhancement,3,EasyCrypt,pre-1.x
17388,allows _ in pattern,,enhancement,3,EasyCrypt,pre-1.x
17390,problem with use of match on expression involving polymorphic operator/abbreviation,,defect,3,EasyCrypt,pre-1.x
17395,potential unsoundness when cloning concrete operators,,defect,3,EasyCrypt,pre-1.x
17396,automated lemmas and simplification hints for match's get_as_X operators,,enhancement,3,EasyCrypt,pre-1.x
17399,`sim: ()` could use `conseq (: )` internally as frame,,enhancement,3,EasyCrypt,pre-1.x
17404,rename procedure name when cloning,,enhancement,3,EasyCrypt,pre-1.x
17406,FEL tactic should take memory reads into account when deciding what counts as an oracle,,defect,3,EasyCrypt,pre-1.x
17407,Alt-Ergo + IntDiv proves false,,defect,3,EasyCrypt,pre-1.x
17410,.eco should include information about provers used,,defect,3,EasyCrypt,pre-1.x
17413,"rewrite /Top.f needed instead of /f to avoid going two levels deep, when op f = T.f",,defect,3,EasyCrypt,pre-1.x
17037,Poor error message for module restriction example,Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
17088,`case !a` should reduce to proving `a`,Pierre-Yves Strub,enhancement,2,EasyCrypt,pre-1.x
17090,Selecting procedure(s) to [inline] by position,,enhancement,2,EasyCrypt,pre-1.x
16912,"Lifting the ""collection update"" statements to tuples",,enhancement,1,EasyCrypt,pre-1.x
17036,Instantiating abstract modules: warnings and interactive justification,,enhancement,1,EasyCrypt,pre-1.x
17045,Rewriting procedures in probability expressions directly from an equivalence,,enhancement,1,EasyCrypt,pre-1.x
17183,Variant of `sim` that works modulo inlining.,,enhancement,1,EasyCrypt,pre-1.x
17297,Allow the optional use of undeclared variables in procedures,,enhancement,1,EasyCrypt,pre-1.x
17307,Coq style Locate,,enhancement,1,EasyCrypt,pre-1.x
17353,"`&&` could disappear from internal code, and be replaced by distinct splitting lemmas for `/\`",,enhancement,1,EasyCrypt,pre-1.x
17356,Two-sided `rcondx`,,enhancement,1,EasyCrypt,pre-1.x
17182,Renaming internal symbols on cloning,Pierre-Yves Strub,enhancement,3,EasyCrypt,pre-1.x
17186,using [bypr] in odd way can result in badly formed goal,Pierre-Yves Strub,defect,3,EasyCrypt,pre-1.x