Custom query (541 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (401 - 500 of 541)

1 2 3 4 5 6

Status: closed (52 matches)

Ticket Summary Owner Type Priority Component Version
#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
#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
#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
#15762 Tactic to transform a tuple equality into a conjonction Pierre-Yves Strub enhancement 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
#17299 Transitivity using an equiv enhancement 3 EasyCrypt phl
#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
#17224 type declarations with bad type variables yield anomalies rather than error messages Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15737 Type-soundness issue when implementing module signatures Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15738 Typing functor applications inside modules Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16288 uncatched exception with functor inside functor Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15852 Undo immediately after 'save.' does not work Pierre-Yves Strub defect 1 ProofGeneral pre-1.x
#17096 Unfolding should work even in the presence of several matching operators. Pierre-Yves Strub enhancement 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
#17106 Unification should work modulo delta-unfolding / simplification. enhancement 3 EasyCrypt pre-1.x
#15908 Unification variables appear Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16137 universal elimination doesn't enforce { ... } restriction on module Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17112 `unknown symbol Top.o` when importing a theory including objects referring to `Top.o` Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17168 Unsoundness: combination of sections, modules, and choice-operators Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17132 Unsoundness in definition of "glob M" Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17114 Unsoundness of module system Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17027 [Unsoundness] The HL and pHL tactics for abstract function calls do not quantify over variables that may be modified in the postcondition Pierre-Yves Strub defect 5 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
#17327 Variants of `<*>` with preference 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
#17177 View application fails non gracely when it cannot instanciate all type variables. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16374 Visual weak-check indicator enhancement 1 ProofGeneral pre-1.x
#16964 Warn when a variable is used before being initialized Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16772 Weird error with inductives when aliasing constructors Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17232 weirdness involving redefining (=) or defining (<>) 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
#17061 when arguments to seq are too big, anomaly rather than error message defect 3 EasyCrypt pre-1.x
#16986 "while >=" generates invalid goals ckunz defect 3 EasyCrypt pre-1.x
#15879 While one sided ckunz enhancement 3 EasyCrypt pre-1.x
#17362 wildcard syntax for SMT provers in prover [...] enhancement 3 EasyCrypt pre-1.x
#17350 witness not in apRHL defect 3 EasyCrypt pre-1.x
#17272 Wrong name defect 3 EasyCrypt pre-1.x
#15910 Wrong precedence for negation "!" Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17214 Wrong printed for memory 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
#15676 Zeta tactics takes too much time to end(infinite loop ?) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x

Status: new (48 matches)

Ticket Summary Owner Type Priority Component Version
#17367 abbreviations involving modules and memories enhancement 3 EasyCrypt pre-1.x
#17383 abstract operators in section should be generalized enhancement 3 EasyCrypt pre-1.x
#17202 Add seq* tactic enhancement 3 EasyCrypt pre-1.x
#17388 allows _ in pattern enhancement 3 EasyCrypt pre-1.x
#17297 Allow the optional use of undeclared variables in procedures enhancement 1 EasyCrypt pre-1.x
#17169 Anonymous functor arguments: passing procedures to functors directly enhancement 3 EasyCrypt pre-1.x
#17358 A normalization operator enhancement 3 EasyCrypt pre-1.x
#17301 Applicative view for `if then else` enhancement 3 EasyCrypt pre-1.x
#17197 Asserts in equivalence proofs enhancement 3 EasyCrypt pre-1.x
#17368 atomic formula of ambient logic expressing disjoint globals of modules enhancement 3 EasyCrypt pre-1.x
#17267 `auto` with `call` enhancement 3 EasyCrypt pre-1.x
#17164 behavior of -check-all enhancement 3 EasyCrypt pre-1.x
#17002 Better section && cloning support Pierre-Yves Strub task 3 EasyCrypt pre-1.x
#17342 Better support for rewriting with equivalences enhancement 3 EasyCrypt pre-1.x
#17282 call should not work task 3 EasyCrypt phl
#17349 call tactic for aequiv conclusions enhancement 3 EasyCrypt pre-1.x
#17088 `case !a` should reduce to proving `a` Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17391 case works with tuple corresponding to glob M, but not with glob M defect 3 EasyCrypt pre-1.x
#17340 cfold should support variables (and more general terms). enhancement 3 EasyCrypt pre-1.x
#17370 checking memory initialisation constraints enhancement 3 EasyCrypt pre-1.x
#17163 Check that `phoare` tactics are forcing the input bounds to be in [0..1]. task 4 EasyCrypt pre-1.x
#17363 Conseq: do not how to combine equivF and hoareS and hoareS into equivS enhancement 3 EasyCrypt pre-1.x
#17307 Coq style Locate enhancement 1 EasyCrypt pre-1.x
#17353 `&&` could disappear from internal code, and be replaced by distinct splitting lemmas for `/\` enhancement 1 EasyCrypt pre-1.x
#17366 crush losing some context on intermediate substitutions defect 3 EasyCrypt pre-1.x
#17386 crush reduces goal whose conclusion is `y1 = y2 <=> x1 = x2` to false goal defect 3 EasyCrypt pre-1.x
#17113 Decide what to do on rewrite with defined head symbols enhancement 3 EasyCrypt pre-1.x
#17175 Direct intro on negative goals enhancement 3 EasyCrypt pre-1.x
#17288 EasyCrypt crashes when printing required abstract theory IterProc defect 3 EasyCrypt pre-1.x
#17149 Expand glob A for concrete module enhancement 3 EasyCrypt pre-1.x
#17225 Explore reproducible smt calls enhancement 3 EasyCrypt pre-1.x
#17341 for loops enhancement 3 EasyCrypt pre-1.x
#17245 Formula manipulation commands (for `conseq` and `seq`) enhancement 3 EasyCrypt pre-1.x
#17086 Generalize [rewrite Pr] enhancement 3 EasyCrypt pre-1.x
#17085 Generic Notations Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17382 glob M should reduce to a record enhancement 3 EasyCrypt pre-1.x
#17346 have access to notation in ml defect 3 EasyCrypt pre-1.x
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` enhancement 3 EasyCrypt pre-1.x
#17036 Instantiating abstract modules: warnings and interactive justification enhancement 1 EasyCrypt pre-1.x
#17348 Intro-pattern `|>` might transform a provable goal to a non-provable one defect 3 EasyCrypt pre-1.x
#17215 Issues with module typing when functor parameters are themselves functors defect 3 EasyCrypt pre-1.x
#17257 `/=` is too weak. defect 3 EasyCrypt pre-1.x
#16912 Lifting the "collection update" statements to tuples enhancement 1 EasyCrypt pre-1.x
#17295 local ops enhancement 3 EasyCrypt pre-1.x
#16648 Make notations and tactics on distributions and functions a bit more uniform. enhancement 3 EasyCrypt pre-1.x
#17384 module parametrised by expressions enhancement 3 EasyCrypt pre-1.x
#16987 Move facts from precondition to context enhancement 3 EasyCrypt pre-1.x
#17239 Mutual inductive types. enhancement 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.