Custom query (541 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (501 - 541 of 541)

1 2 3 4 5 6

Status: new (39 matches)

Ticket Summary Owner Type Priority Component Version
#17257 `/=` is too weak. defect 3 EasyCrypt pre-1.x
#17251 print Self enhancement 3 EasyCrypt pre-1.x
#17246 `rewrite`, apply, ... in contracts defect 3 EasyCrypt pre-1.x
#17245 Formula manipulation commands (for `conseq` and `seq`) enhancement 3 EasyCrypt pre-1.x
#17239 Mutual inductive types. enhancement 3 EasyCrypt pre-1.x
#17225 Explore reproducible smt calls enhancement 3 EasyCrypt pre-1.x
#17218 proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate enhancement 3 EasyCrypt pre-1.x
#17217 need better error message when attempting to apply lemma to goal that isn't a judgment enhancement 3 EasyCrypt pre-1.x
#17215 Issues with module typing when functor parameters are themselves functors defect 3 EasyCrypt pre-1.x
#17210 Pattern-matching for pairs in operator arguments enhancement 3 EasyCrypt pre-1.x
#17202 Add seq* tactic enhancement 3 EasyCrypt pre-1.x
#17197 Asserts in equivalence proofs enhancement 3 EasyCrypt pre-1.x
#17192 Problem with `glob` and type inference defect 3 EasyCrypt pre-1.x
#17183 Variant of `sim` that works modulo inlining. enhancement 1 EasyCrypt pre-1.x
#17175 Direct intro on negative goals enhancement 3 EasyCrypt pre-1.x
#17169 Anonymous functor arguments: passing procedures to functors directly enhancement 3 EasyCrypt pre-1.x
#17164 behavior of -check-all 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
#17156 New vernacular command: `print axiom` enhancement 3 EasyCrypt pre-1.x
#17149 Expand glob A for concrete module enhancement 3 EasyCrypt pre-1.x
#17140 Pattern matching should make use of simplification rules. enhancement 3 EasyCrypt pre-1.x
#17136 variant of seq to deal with large preconditions enhancement 3 EasyCrypt pre-1.x
#17113 Decide what to do on rewrite with defined head symbols enhancement 3 EasyCrypt pre-1.x
#17105 [transitivity] for phoare and hoare enhancement 3 EasyCrypt pre-1.x
#17090 Selecting procedure(s) to [inline] by position enhancement 2 EasyCrypt pre-1.x
#17088 `case !a` should reduce to proving `a` Pierre-Yves Strub enhancement 2 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
#17082 SMT tactic should be interruptable. Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#17077 No more direct access to stdlib paths Pierre-Yves Strub defect 4 Internals pre-1.x
#17045 Rewriting procedures in probability expressions directly from an equivalence enhancement 1 EasyCrypt pre-1.x
#17037 Poor error message for module restriction example Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17036 Instantiating abstract modules: warnings and interactive justification enhancement 1 EasyCrypt pre-1.x
#17022 Pattern-matching on variables in judgments and probability expressions enhancement 3 EasyCrypt pre-1.x
#17002 Better section && cloning support Pierre-Yves Strub task 3 EasyCrypt pre-1.x
#16987 Move facts from precondition to context enhancement 3 EasyCrypt pre-1.x
#16912 Lifting the "collection update" statements to tuples enhancement 1 EasyCrypt pre-1.x
#16648 Make notations and tactics on distributions and functions a bit more uniform. enhancement 3 EasyCrypt pre-1.x
#16103 scoping issue with theories enhancement 3 EasyCrypt pre-1.x

Status: reopened (2 matches)

Ticket Summary Owner Type Priority Component Version
#17186 using [bypr] in odd way can result in badly formed goal Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17182 Renaming internal symbols on cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
1 2 3 4 5 6
Note: See TracQuery for help on using queries.