Custom query (531 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (1 - 100 of 531)

1 2 3 4 5 6

Status: accepted (11 matches)

Ticket Summary Owner Type Priority Component Version
#16113 <top> in printer Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17024 Pattern matching should try to infer memory and module parameters Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17034 Generalizing loop fusion Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17040 Syntactic sugar for nested if-then-else statements. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17042 Pattern matching in non-normal form. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17070 better error message when difference between goal and lemma is tiny Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17195 Swap with 2 args move as far down as possible Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17250 off-by-one error in swap Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17309 `rewrite /F` when F is a fixpoint should simplify selected occurence for head-iota reduction. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17141 Wrong module type annotations accepted Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17378 Proof of false using smt and Eprover. Pierre-Yves Strub defect 5 EasyCrypt pre-1.x

Status: assigned (28 matches)

Ticket Summary Owner Type Priority Component Version
#17343 (Optional) warning for old syntax Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17345 Bad printing Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#17364 Internals: use Batteries maps instead of Why3 ones. Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17117 Warning when restrictions over an adversary are empty Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
#17160 Call SMT in parallels. Pierre-Yves Strub enhancement 2 Internals pre-1.x
#17253 EasyCrypt should fail gracefully when applying a tactic on a solved goal. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17264 Add the possibility to clear lemmas when closing a theory. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17310 Top-level command to print various databases (exact, rewrite, ...) Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17347 Search with notations is broken. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17181 slow rewriting for large expressions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17194 anomaly: EcHiGoal.LowApply.NoInstance (in byequiv) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17207 Applicative view Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17222 local clones do not disappear from the environment on section end Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17240 Syntactic sugar for proc. that reduces to a call to an external proc. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17255 Missing unification in `clone...with...` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17256 apply/rewrite should work modulo zeta-reduction. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17261 `rewrite -/(f _)` should not match its own unfoldings. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17262 Add the possibility to add rewrite hints to rewrite hint databases. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17263 Multiple incompleteness in `apply` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17265 `goal` vernacular command Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17268 Add a tactical that fails when no progress is done. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17269 Add notations for >/>= Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17270 `done` should close a goal when `false` is a local hyp. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17271 Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17308 `rewrite !(A,B)` loops when `B` is not known about Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17319 Anomaly triggered by `smt` defect 3 EasyCrypt pre-1.x
#17334 this message need more information: cannot infer all placeholders Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17335 the formula contains free type variables Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x

Status: closed (61 matches)

Ticket Summary Owner Type Priority Component Version
#15612 require Theory issues misleading "added" messages Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#15852 Undo immediately after 'save.' does not work Pierre-Yves Strub defect 1 ProofGeneral pre-1.x
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#16374 Visual weak-check indicator enhancement 1 ProofGeneral pre-1.x
#16885 Support for type annotations in let expressions Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17071 Error message for [expect] <default> enhancement 1 EasyCrypt pre-1.x
#17104 Make (<>) accessible in prefix form enhancement 1 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
#17204 Syntax for ignoring the return value of a procedure call Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17294 `Self` (and `Top`) should be allowed in module restrictions Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#15106 Consider probability quantities as real-valued expressions enhancement 2 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
#15817 Lighten EC syntax by removing the clumsy "<:" && "&" notations for modules / memories introductions / applications Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15873 Bug Printer Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#15906 (local) opening of modules Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15910 Wrong precedence for negation "!" Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#15912 Be able to inline only one side after an equiv Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15915 conjunctive introduction pattern does not split <=> 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
#15930 Clear all Pierre-Yves Strub enhancement 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
#15999 Pretty printer add too much scoping annotations. 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
#16087 New view for apply: !a -> (a => false) Pierre-Yves Strub enhancement 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
#16457 try tactic not catching case failure Pierre-Yves Strub defect 2 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
#16504 Parse error on complex arguments to functions in probability statements Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#16622 Functor-level "lambdas" Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
#16663 Goal window should update on tactic failure... Pierre-Yves Strub defect 2 ProofGeneral pre-1.x
#16746 Losslessness annotations Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#16773 "do! rewrite /op" loops Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17007 Inconsistent syntax for closing sections/theories enhancement 2 EasyCrypt pre-1.x
#17011 Pretty-printer in adding too much scoping annotation Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17026 EasyCrypt does not compile on Windows (win32 / cygwin) Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17049 "restart scripting" not working in ProofGeneral defect 2 ProofGeneral pre-1.x
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 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
#17110 [anomaly] on using [call] with a lemma referring to the wrong procedure Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17199 PG: Default weak-check mode indicator is invalid. Pierre-Yves Strub defect 2 ProofGeneral pre-1.x
#17227 Procedures with unit return type should be allowed to return `tt' Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17249 `AlgTactic` && `Ring` should agree on their axioms. 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
#17369 imprecise pretty printing with functor application defect 2 EasyCrypt pre-1.x
#17381 Possible bug: no matching operator even when available defect 2 EasyCrypt pre-1.x
#15502 "Ident <top>_[...] is not yet declared" when cloning a theory with operators Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15506 Issues when cloning theories Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15520 request for more loop manipulation tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15647 Can't extract easily function from tuple Pierre-Yves Strub defect 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.