Custom query (541 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (101 - 200 of 541)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Component Version
#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
#17332 Better localisation when a pattern cannot be infered 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
#16512 Bug in pose 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
#15814 call tactic accepts variable defined in left game ({1}) defined for right game 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
#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
#15930 Clear all 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
#17122 Clone ignores provided proof Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15907 clone import and clone export Pierre-Yves Strub enhancement 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
#17393 Cloning polymorphic datatypes does not allow case analysis defect 3 EasyCrypt pre-1.x
#16629 cloning within sections Pierre-Yves Strub enhancement 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
#15915 conjunctive introduction pattern does not split <=> Pierre-Yves Strub defect 2 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
#15106 Consider probability quantities as real-valued expressions enhancement 2 EasyCrypt pre-1.x
#15880 Constant propagation with module variable Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16737 "declare op" 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
#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
#16775 EasyCrypt insists on typing boolean-returning fixpoints as predicates Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17329 EasyCrypt output (goals order e.g.) is not stable Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17078 EasyCrypt should use big integers internally. Pierre-Yves Strub defect 3 Internals pre-1.x
#17013 EasyCrypt toolchain does not compile anymore on OSX Pierre-Yves Strub defect 5 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
#17050 elim/let anomaly 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
#17071 Error message for [expect] <default> enhancement 1 EasyCrypt pre-1.x
#15702 Error with multiple require if they contain the same game Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17236 error with rewriting occurrence of -1 when only one matching occurrence defect 3 EasyCrypt pre-1.x
#17188 Error with smt : lazy defect 3 EasyCrypt pre-1.x
#17278 [eta] reduction is not full on multi-ary functions github <noreply@…> defect 3 EasyCrypt pre-1.x
#17115 [exfalso] tactic for ambient logic enhancement 3 EasyCrypt pre-1.x
#17159 expect should support goal selection Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15916 Extraneous internal memory identifier "hr" in output 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
#17237 failure of rewrite ... in ... Pierre-Yves Strub 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
#17302 fel can generate subgoal with undefined memory Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16416 FEL completeness - initialization Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17054 Finiteness of product of finite types enhancement 3 Libraries 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
#16165 "fixed" a breaking test case that may have been left as a TODO Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17155 Fix stdlib w.r.t. why3 import Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17158 "<-" for predicates when cloning 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
#17100 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16222 Functor application circumvents section-locality Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16622 Functor-level "lambdas" Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
#15872 fun stopped working ckunz defect 5 EasyCrypt pre-1.x
#16231 General issues with computation of globals for nested modules Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16990 Generalization does not cross tuple projections. 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
#17119 Give the ability to print subgoals Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.