Custom query (412 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (201 - 300 of 412)

1 2 3 4 5

Resolution: fixed (100 matches)

Ticket Summary Owner Type Priority Component Version
#17241 `clone import` not working when realizing axioms. Pierre-Yves Strub defect 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
#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
#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 <noreply@…> defect 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
#17294 `Self` (and `Top`) should be allowed in module restrictions Pierre-Yves Strub defect 1 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
#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
#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
#17329 EasyCrypt output (goals order e.g.) is not stable Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17330 anomaly on `apply/contra` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17339 `anomaly: EcLowGoal.InvalidProofTerm.` on `/>` Pierre-Yves Strub defect 4 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
#17365 Proof of false using Ring and Reals. Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17369 imprecise pretty printing with functor application defect 2 EasyCrypt pre-1.x
#17373 introduction pattern bug somehow related to SmtMap defect 3 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
#17385 problem sending goal to SMT (involving inductive datatype and higher order function) Pierre-Yves Strub 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
#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
#15949 Improve kill error message Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 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
#16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#16104 naming issues enhancement 3 EasyCrypt pre-1.x
#16416 FEL completeness - initialization Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#16725 Intro pattern for substitution 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
#16786 Nicer treatment of datatype constructors 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
#17005 Higher-order pattern matching enhancement 3 EasyCrypt pre-1.x
#17007 Inconsistent syntax for closing sections/theories enhancement 2 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
#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
#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
#17071 Error message for [expect] <default> enhancement 1 EasyCrypt pre-1.x
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 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
#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
#17087 [conseq*] should be the default behaviour of [conseq] Pierre-Yves Strub enhancement 4 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
#17093 Add the possibility to declare several operators/predicates in 1 command. Pierre-Yves Strub enhancement 2 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
#17098 Add a search facility Pierre-Yves Strub enhancement 4 Documentation 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
#17106 Unification should work modulo delta-unfolding / simplification. enhancement 3 EasyCrypt pre-1.x
#17119 Give the ability to print subgoals Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17126 Command and command line option for global timeout multiplier. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17130 "alias i" works only on random instruction. Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17137 More tactical about goal selections Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17139 Multiple require at once. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17151 Abstract theories Pierre-Yves Strub enhancement 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
#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
#17176 [print] should display types even on fixpoints Pierre-Yves Strub enhancement 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
#17185 Anomalies should give rise to a "This is a bug, please report."-type message. Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17189 Syntax for referring to *local* variables by their long name Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17196 Vernacular command for dumping env. as a Why3 task. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17201 `x-y` and `x + -y` should be convertible Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17204 Syntax for ignoring the return value of a procedure call Pierre-Yves Strub enhancement 1 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.