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
#17009 1.x error messages Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17151 Abstract theories Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17098 Add a search facility Pierre-Yves Strub enhancement 4 Documentation pre-1.x
#17093 Add the possibility to declare several operators/predicates in 1 command. Pierre-Yves Strub enhancement 2 EasyCrypt 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
#17249 `AlgTactic` && `Ring` should agree on their axioms. Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17273 `alias` failures look like uncaught exceptions defect 3 EasyCrypt pre-1.x
#17130 "alias i" works only on random instruction. Benjamin Grégoire enhancement 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
#17124 allows to specify timeout only for smt. 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
#17035 Alt-Ergo succeeds on false obligations in weird circumstances Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17372 "" and "!" semantic for smt Pierre-Yves Strub enhancement 3 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
#16984 Anomaly due to inlining functions with tuple arguments Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17339 `anomaly: EcLowGoal.InvalidProofTerm.` on `/>` Pierre-Yves Strub defect 4 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
#17143 Anomaly (free type variables in conseq) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17089 anomaly in [sim] Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#17292 anomaly on application of a `<=>` lemma to a `=` goal defect 3 EasyCrypt pre-1.x
#17330 anomaly on `apply/contra` Pierre-Yves Strub defect 3 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
#17142 Anomaly (related to SMT and memories) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17320 anomaly when cloning theory with inductive predicate Pierre-Yves Strub defect 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
#17135 anomaly when intro pattern has wrong form 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
#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
#17238 anomaly with auto-revert intro pattern Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16788 Another stack overflow during unification 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
#17128 assert false in rnd. Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15924 Assertion failed in otherwise provable goal Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15965 Assertion failure in EcEnv Pierre-Yves Strub 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
#16362 Assertion failure when cloning a theory with let expressions Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16114 Bad error message Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17116 Bad error message for [swap] 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
#16067 bad error message when value is treated as function 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
#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
#17162 Bad interaction between abstract theories and local modules Pierre-Yves Strub defect 4 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
#17123 Bad parsing on call (_: B, I) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17097 Bad pretty-printing of lists. 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
#17376 behaviour of module type include in functor types Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17066 Better error message when operator selection failed. 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
#16856 Blocker typing bug in rnd (master) 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
#16849 Broken proc (in branch 1.0) 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
#16692 bug in apply. Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#16174 Bug in bdhoare call ckunz defect 3 EasyCrypt pre-1.x
#16306 Bug in cloning ? Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#16399 Bug in congr? Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15842 Bug in lambda translation Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16656 bug in parser with rewrite? Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16264 Bug in rewrite with let 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
#16013 Bug in theory realization Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15781 Bug into env insertion of a specific axiom Pr[] Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17127 Bug in typing of instruction x.[y] = e; Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#15873 Bug Printer Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#16790 Bug when cloning and instantiating an abstract type Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15893 Call in adversary call is not working properly Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#15813 call tactic signals an "unknown symbol" error 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
#17125 Cannot clear variables referring to memory 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
#15647 Can't extract easily function from tuple 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
#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
#15919 [case] tactic for bd_hoare is useless 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
#17092 Chaining [apply] Pierre-Yves Strub enhancement 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
#17377 characterization lemmas for <=> and \proper 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
#17145 "choice" reorders its arguments 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
#17266 Clear goal window when no more goals Pierre-Yves Strub enhancement 2 ProofGeneral pre-1.x
#17122 Clone ignores provided proof 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
#17318 clone-time regexp substitution should apply in the specified order 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
#17274 Collision in names, local variables unreachable 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
#15881 Complete path for local variable in printer 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
#17275 [congr] should apply to iff Pierre-Yves Strub 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
#17087 [conseq*] should be the default behaviour of [conseq] Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#15981 "delta cpEq" causes an untypable goal to be produced Benjamin Grégoire 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
#16773 "do! rewrite /op" loops Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17138 "easycrypt -check-all" does not load "Logic" Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17026 EasyCrypt does not compile on Windows (win32 / cygwin) Pierre-Yves Strub defect 2 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.