id Summary Owner Type Priority Component Version
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
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
15702 Error with multiple require if they contain the same game Pierre-Yves Strub defect 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
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
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
15506 Issues when cloning theories Pierre-Yves Strub defect 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
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
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
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
15813 "call tactic signals an ""unknown symbol"" error" 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
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
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
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
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
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
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
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
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
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
16231 General issues with computation of globals for nested modules Benjamin Grégoire 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
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
16468 try fails to catch some call-related exceptions defect 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
16656 bug in parser with rewrite? Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
16691 the name should be accessible to the user. Pierre-Yves Strub defect 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
16751 hoare should work on fun. Benjamin Grégoire defect 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
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
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
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
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
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
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
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
17116 Bad error message for [swap] Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
17119 Give the ability to print subgoals Pierre-Yves Strub 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
17135 anomaly when intro pattern has wrong form Pierre-Yves Strub defect 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
15815 Search path for theories should include path of currently active file Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
15873 Bug Printer Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
15910 "Wrong precedence for negation ""!""" 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
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
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
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
16504 Parse error on complex arguments to functions in probability statements Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
16663 Goal window should update on tactic failure... Pierre-Yves Strub defect 2 ProofGeneral 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
17369 imprecise pretty printing with functor application defect 2 EasyCrypt pre-1.x
15612 "require Theory issues misleading ""added"" messages" Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
17071 Error message for [expect] 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
17155 Fix stdlib w.r.t. why3 import Pierre-Yves Strub defect 4 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
16253 Non-local modules and abstract restrictions. defect 3 EasyCrypt pre-1.x
16512 Bug in pose Pierre-Yves Strub 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
17107 "Potential mismatch between spec and lemma versions of the ""pHL + HL => pHL"" variant of [conseq]" 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
17191 Assert failure 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
17272 Wrong name defect 3 EasyCrypt pre-1.x
17289 Missing dependencies in OPAM package defect 3 EasyCrypt pre-1.x
15915 conjunctive introduction pattern does not split <=> 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
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
15884 Repeat tactic broken 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
17115 [exfalso] tactic for ambient logic enhancement 3 EasyCrypt pre-1.x
17121 Make Option.witness accessible at top level enhancement 3 EasyCrypt pre-1.x
17232 weirdness involving redefining (=) or defining (<>) enhancement 3 EasyCrypt pre-1.x
17350 witness not in apRHL 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
15852 Undo immediately after 'save.' does not work Pierre-Yves Strub defect 1 ProofGeneral pre-1.x
16374 Visual weak-check indicator enhancement 1 ProofGeneral pre-1.x
17104 Make (<>) accessible in prefix form enhancement 1 EasyCrypt pre-1.x
15520 request for more loop manipulation tactics 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
16229 Substitution issue when quantified module variables have the same name as an existing module 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
16737 """declare op""" Pierre-Yves Strub enhancement 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
17108 require clone enhancement 3 EasyCrypt pre-1.x
17118 Add the ability to print the axioms of the environment 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
17146 Bad error message in combination choice/modules/section Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
17154 anomaly: EcPV.MemoryClash 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
17332 Better localisation when a pattern cannot be infered Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
17052 Parse error on (**) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
17095 anomaly raised by invariant form of [call upto] 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
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
15106 Consider probability quantities as real-valued expressions enhancement 2 EasyCrypt pre-1.x
15891 Instantiating axioms and sub-theories when cloning theories Pierre-Yves Strub enhancement 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
15716 Problem with introduction of Module in Proof 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
15779 Inference during apply Pierre-Yves Strub enhancement 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
15849 Ignoring proof that are already done in a file Pierre-Yves Strub enhancement 3 EasyCrypt 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
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
15907 clone import and clone export Pierre-Yves Strub enhancement 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
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
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
16082 move * for adversary function outside { ... } Pierre-Yves Strub enhancement 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
16456 allow expression, formula in cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
16560 Non-relational 'bypr' for probabilistic Hoare statements ckunz enhancement 3 EasyCrypt pre-1.x
16657 Pattern-matching on records Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
16723 Subtyping for abstract modules and functors Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
16749 link between hoare bdhoare equiv Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
16763 Simplification should discriminate datatype constructors Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
16789 Pattern matching should to some top-level delta-unfolding Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
16918 "selection tactical ""all n""" Pierre-Yves Strub enhancement 3 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
15906 (local) opening of modules Pierre-Yves Strub enhancement 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
15930 Clear all Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
16087 New view for apply: !a -> (a => false) Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
16622 "Functor-level ""lambdas""" Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
16746 Losslessness annotations Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
16885 Support for type annotations in let expressions Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x