Custom query (405 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (1 - 100 of 405)

1 2 3 4 5

Resolution: fixed (100 matches)

Ticket Summary Owner Type Priority Component Version
#17252 The `seq` variant documented as pHL is in fact the HL tactic. Alley Stoughton defect 3 Documentation 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
#15893 Call in adversary call is not working properly Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#15919 [case] tactic for bd_hoare is useless Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 EasyCrypt pre-1.x
#15974 The following example generates an anomaly Benjamin Grégoire 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
#16000 repeated instantiation and losslessness of 3-argument fun don't work well together Benjamin Grégoire 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
#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
#16306 Bug in cloning ? Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#16362 Assertion failure when cloning a theory with let expressions Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16416 FEL completeness - initialization Benjamin Grégoire enhancement 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
#16787 new conseq issues Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#16849 Broken proc (in branch 1.0) Benjamin Grégoire defect 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
#17021 Some judgment-combining variants of conseq do not apply to procedures Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17083 Missing eta-reduction in conversion Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17089 anomaly in [sim] Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#17109 Hoare adversary rule introducess references to non-existent memories in postconditions Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17114 Unsoundness of module system Benjamin Grégoire defect 5 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
#17142 Anomaly (related to SMT and memories) Benjamin Grégoire 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
#17376 behaviour of module type include in functor types Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#15872 fun stopped working ckunz defect 5 EasyCrypt pre-1.x
#16174 Bug in bdhoare call ckunz defect 3 EasyCrypt pre-1.x
#16986 "while >=" generates invalid goals ckunz defect 3 EasyCrypt pre-1.x
#17071 Error message for [expect] <default> enhancement 1 EasyCrypt pre-1.x
#17278 [eta] reduction is not full on multi-ary functions github <noreply@…> defect 3 EasyCrypt pre-1.x
#15506 Issues when cloning theories Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15612 require Theory issues misleading "added" messages Pierre-Yves Strub defect 1 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
#15702 Error with multiple require if they contain the same game Pierre-Yves Strub defect 4 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
#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
#15815 Search path for theories should include path of currently active file Pierre-Yves Strub defect 2 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
#15873 Bug Printer Pierre-Yves Strub defect 2 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
#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
#15924 Assertion failed in otherwise provable goal Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15949 Improve kill error message Pierre-Yves Strub enhancement 2 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
#15975 Cfold bug with notation x.[a] = Pierre-Yves Strub defect 3 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
#15998 Problem in cloning Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16001 Instantiating an internal theory when cloning fails Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16002 bad error message when predicate is given polymorphic constant Pierre-Yves Strub defect 2 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
#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
#16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#16086 Missing error message: "Abstract function <function name> 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
#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
#16114 Bad error message Pierre-Yves Strub defect 2 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
(more results for this group on next page)
1 2 3 4 5
Note: See TracQuery for help on using queries.