Custom query (536 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (1 - 100 of 536)

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
#17141 Wrong module type annotations accepted Pierre-Yves Strub defect 4 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
#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
#17319 Anomaly triggered by `smt` defect 3 EasyCrypt pre-1.x
#17160 Call SMT in parallels. Pierre-Yves Strub enhancement 2 Internals pre-1.x
#17181 slow rewriting for large expressions Pierre-Yves Strub 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
#17253 EasyCrypt should fail gracefully when applying a tactic on a solved goal. Pierre-Yves Strub defect 2 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
#17264 Add the possibility to clear lemmas when closing a theory. Pierre-Yves Strub defect 2 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
#17310 Top-level command to print various databases (exact, rewrite, ...) Pierre-Yves Strub defect 2 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
#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
#17347 Search with notations is broken. Pierre-Yves Strub defect 2 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
#17194 anomaly: EcHiGoal.LowApply.NoInstance (in byequiv) Benjamin Grégoire defect 3 EasyCrypt pre-1.x

Status: closed (61 matches)

Ticket Summary Owner Type Priority Component Version
#15106 Consider probability quantities as real-valued expressions enhancement 2 EasyCrypt pre-1.x
#15786 Swap with call to the adversary defect 3 EasyCrypt pre-1.x
#16058 Syntax f.x in equiv precondition for fonction argument enhancement 3 EasyCrypt pre-1.x
#16104 naming issues enhancement 3 EasyCrypt pre-1.x
#16229 Substitution issue when quantified module variables have the same name as an existing module defect 3 EasyCrypt pre-1.x
#16253 Non-local modules and abstract restrictions. defect 3 EasyCrypt pre-1.x
#16374 Visual weak-check indicator enhancement 1 ProofGeneral pre-1.x
#16468 try fails to catch some call-related exceptions defect 3 EasyCrypt pre-1.x
#16628 making nested sections work 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
#17047 pretty printing of module type uses old notation for "*" defect 3 EasyCrypt pre-1.x
#17049 "restart scripting" not working in ProofGeneral defect 2 ProofGeneral pre-1.x
#17051 Pretty-printing regression defect 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
#17060 pretty printer still using "lambda" instead of "fun" defect 3 EasyCrypt pre-1.x
#17061 when arguments to seq are too big, anomaly rather than error message defect 3 EasyCrypt pre-1.x
#17095 anomaly raised by invariant form of [call upto] defect 3 EasyCrypt pre-1.x
#17104 Make (<>) accessible in prefix form enhancement 1 EasyCrypt pre-1.x
#17106 Unification should work modulo delta-unfolding / simplification. enhancement 3 EasyCrypt pre-1.x
#17107 Potential mismatch between spec and lemma versions of the "pHL + HL => pHL" variant of [conseq] defect 3 EasyCrypt pre-1.x
#17108 require clone enhancement 3 EasyCrypt pre-1.x
#17115 [exfalso] tactic for ambient logic enhancement 3 EasyCrypt pre-1.x
#17118 Add the ability to print the axioms of the environment enhancement 3 EasyCrypt pre-1.x
#17121 Make Option.witness accessible at top level enhancement 3 EasyCrypt pre-1.x
#17154 anomaly: EcPV.MemoryClash defect 3 EasyCrypt pre-1.x
#17173 alternative to "require A; clone export A as B" that does not add A to SMT context enhancement 3 EasyCrypt pre-1.x
#17174 Return of the memory explosion defect 3 EasyCrypt pre-1.x
#17188 Error with smt : lazy defect 3 EasyCrypt pre-1.x
#17216 All test suites should include abstract theory files (*.eca) defect 3 Internals pre-1.x
#17232 weirdness involving redefining (=) or defining (<>) enhancement 3 EasyCrypt pre-1.x
#17236 error with rewriting occurrence of -1 when only one matching occurrence defect 3 EasyCrypt pre-1.x
#17254 print produces misleading results on partially applied functors defect 3 EasyCrypt pre-1.x
#17272 Wrong name defect 3 EasyCrypt pre-1.x
#17273 `alias` failures look like uncaught exceptions defect 3 EasyCrypt pre-1.x
#17289 Missing dependencies in OPAM package defect 3 EasyCrypt pre-1.x
#17292 anomaly on application of a `<=>` lemma to a `=` goal defect 3 EasyCrypt pre-1.x
#17296 Some program tactics (`rnd`) generate invalid formulas when Distr is not loaded defect 3 EasyCrypt pre-1.x
#17299 Transitivity using an equiv enhancement 3 EasyCrypt phl
#17315 [print] on notations is not very useful defect 3 EasyCrypt pre-1.x
#17328 `_` intro-pattern should only check if the clear is possible once the rest of the intro-pattern has been processed enhancement 3 EasyCrypt pre-1.x
#17350 witness not in apRHL defect 3 EasyCrypt pre-1.x
#17352 Question about run easycrypt task 3 EasyCrypt pre-1.x
#17359 `rewrite ?lem` should fail (hard) if `lem` does not exist in scope enhancement 3 EasyCrypt pre-1.x
#17362 wildcard syntax for SMT provers in prover [...] enhancement 3 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
#17381 Possible bug: no matching operator even when available defect 2 EasyCrypt pre-1.x
#17389 inline does not inline under match statement defect 3 EasyCrypt pre-1.x
#15918 Tactic for proving an equiv/hoare/bd_hoare goal when the pre-condition is contradictory Santiago Zanella-Béguelin enhancement 3 EasyCrypt pre-1.x
#15920 [conseq (_ : pre => _)] tactic for bd_hoare doesn't work Santiago Zanella-Béguelin defect 3 EasyCrypt pre-1.x
#15922 if tactic for bd_hoare doesn't work with precondition true Santiago Zanella-Béguelin defect 3 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
#15612 require Theory issues misleading "added" messages Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#15647 Can't extract easily function from tuple Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15651 lambda in operator doesn't work Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15676 Zeta tactics takes too much time to end(infinite loop ?) 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.