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
#17193 Obscure failure on lazy smt with higher-order stuff and booleans 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
#15794 Operator not found Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17219 operators don't print the way they are declared Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17148 Operators should be subject to section restrictions Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#16963 op/pred nosmt ... Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17200 Parse error in required theories are incorrectly located. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17147 Parse error in (some) expressions involving memories Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17184 parse error involving parameterized module Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16504 Parse error on complex arguments to functions in probability statements Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17280 Parse-only abbreviations 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
#17199 PG: Default weak-check mode indicator is invalid. Pierre-Yves Strub defect 2 ProofGeneral pre-1.x
#17068 Possible bug in the union-find algorithm Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17260 pragma +option should fail gracefully. 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
#17072 Pretty Printer Glitches for !(_ = _) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17011 Pretty-printer in adding too much scoping annotation Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17355 Pretty-printer sometimes forget to use the abbreviation Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17060 pretty printer still using "lambda" instead of "fun" defect 3 EasyCrypt pre-1.x
#17228 pretty printer uses bad syntax for type constructors Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17233 pretty printing issues with _?_:_ and modules Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17047 pretty printing of module type uses old notation for "*" defect 3 EasyCrypt pre-1.x
#17051 Pretty-printing regression defect 3 EasyCrypt pre-1.x
#17012 pr_false is badly implemented (unsoundness) Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#15982 Printer bug for partially applied infix operators in prefix form Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16149 printer bug: parentheses in types Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17315 [print] on notations is not very useful defect 3 EasyCrypt pre-1.x
#17254 print produces misleading results on partially applied functors defect 3 EasyCrypt pre-1.x
#17242 `print` should display `nosmt` info 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
#15998 Problem in cloning Pierre-Yves Strub defect 3 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
#16732 Problem with functor aliases when outermost module is a parameter Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17227 Procedures with unit return type should be allowed to return `tt' Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17190 progress and progress => //. should be equivalent... 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
#17365 Proof of false using Ring and Reals. Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17379 Proving unreasonable/false lemmas through Alt-Ergo defect 5 EasyCrypt pre-1.x
#17352 Question about run easycrypt task 3 EasyCrypt pre-1.x
#17094 Refactoring: code for operators addition. Pierre-Yves Strub enhancement 3 Internals pre-1.x
#17304 Regression on anonymous procedure arguments support Pierre-Yves Strub 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
#15744 require import causes name collisions in sub 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
#17049 "restart scripting" not working in ProofGeneral defect 2 ProofGeneral pre-1.x
#15764 Result not introduce after call in hoare logic 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
#17174 Return of the memory explosion defect 3 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
#17208 `rewrite ... in ...` Pierre-Yves Strub defect 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
#16116 rewrite /op failed with lambda Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17091 [rewrite] should head-reduce created b-redexes Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17203 Rewrite strangely failling Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15996 rewriting when using intro patterns to eliminate existentials Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17120 [rnd] allows to prove false Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#15851 [rnd] for map update produces confusing post-conditions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16112 Rnd on different type possible Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17361 scoping problem with theory renaming 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
#17294 `Self` (and `Top`) should be allowed in module restrictions Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#17153 seq does not check type of its arguments 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
#17021 Some judgment-combining variants of conseq do not apply to procedures Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15966 Something wrong with installation script? Pierre-Yves Strub defect 3 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
#17226 some weirdness with operators of form :+ 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
#17018 splitwhile syntax is still weird Pierre-Yves Strub defect 3 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
#17198 Spurious failure of rewrite Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15871 Stack Overflow Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16726 Stack overflow during unification Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16111 Strange bug in require Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16140 Strange error in typing 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
#16115 Subst failed Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17284 Support for `={<expr>}` in equiv contracts Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15786 Swap with call to the adversary defect 3 EasyCrypt pre-1.x
#17067 Syntax for chained case analysis of the top-assumption 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
#17084 syntax for non-flat proof-terms Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17189 Syntax for referring to *local* variables by their long name 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
#17314 Syntax variants of multiple argument module types don't match ones for parameterized modules Pierre-Yves Strub enhancement 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
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 EasyCrypt pre-1.x
#16729 Tactic swap causes inconsistent dependencies Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17080 `t_generalize_hyps` does not work when given a non-singleton list. Pierre-Yves Strub defect 4 Internals pre-1.x
#15974 The following example generates an anomaly Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16691 the name <top> should be accessible to the user. 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
#17252 The `seq` variant documented as pHL is in fact the HL tactic. Alley Stoughton defect 3 Documentation pre-1.x
#15853 timeout and prover settings are not undone Pierre-Yves Strub defect 3 ProofGeneral pre-1.x
#15990 trivial cannot prove chained relations directly Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#16468 try fails to catch some call-related exceptions defect 3 EasyCrypt pre-1.x
#16457 try tactic not catching case failure Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#15882 tuple and memory misprinted 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.