Custom query (122 matches)


Show under each result:

Results (101 - 122 of 122)

1 2

Status: new (20 matches)

Ticket Summary Owner Type Priority Component Version
#17351 sp for aqeuiv goals enhancement 3 EasyCrypt pre-1.x
#17357 rnd tactic for aprhl enhancement 3 EasyCrypt pre-1.x
#17358 A normalization operator enhancement 3 EasyCrypt pre-1.x
#17363 Conseq: do not how to combine equivF and hoareS and hoareS into equivS enhancement 3 EasyCrypt pre-1.x
#17366 crush losing some context on intermediate substitutions defect 3 EasyCrypt pre-1.x
#17367 abbreviations involving modules and memories enhancement 3 EasyCrypt pre-1.x
#17368 atomic formula of ambient logic expressing disjoint globals of modules enhancement 3 EasyCrypt pre-1.x
#17370 checking memory initialisation constraints enhancement 3 EasyCrypt pre-1.x
#17374 pre-/post- should be implemented with an explicit memory enhancement 3 Internals pre-1.x
#17037 Poor error message for module restriction example Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17088 `case !a` should reduce to proving `a` Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17090 Selecting procedure(s) to [inline] by position enhancement 2 EasyCrypt pre-1.x
#16912 Lifting the "collection update" statements to tuples enhancement 1 EasyCrypt pre-1.x
#17036 Instantiating abstract modules: warnings and interactive justification enhancement 1 EasyCrypt pre-1.x
#17045 Rewriting procedures in probability expressions directly from an equivalence enhancement 1 EasyCrypt pre-1.x
#17183 Variant of `sim` that works modulo inlining. enhancement 1 EasyCrypt pre-1.x
#17297 Allow the optional use of undeclared variables in procedures enhancement 1 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
#17356 Two-sided `rcondx` enhancement 1 EasyCrypt pre-1.x

Status: reopened (2 matches)

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