Custom query (405 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (201 - 300 of 405)

1 2 3 4 5

Resolution: fixed (100 matches)

Ticket Summary Owner Type Priority Component Version
#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 <noreply@…> defect 3 EasyCrypt pre-1.x
#17280 Parse-only abbreviations Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17284 Support for `={<expr>}` 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 <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
#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
(more results for this group on next page)
1 2 3 4 5
Note: See TracQuery for help on using queries.