Custom query (429 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (401 - 429 of 429)

1 2 3 4 5

Resolution: None (27 matches)

Ticket Summary Owner Type Priority Component Version
#15859 Omit path when it can be inferred from context Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15879 While one sided ckunz enhancement 3 EasyCrypt pre-1.x
#15880 Constant propagation with module variable Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15907 clone import and clone export Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15917 Proving "a = b => f a = f b" should not require a call to SMT 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
#15921 A strongest post-condition tactic [sp n m], like in trunk ckunz enhancement 3 EasyCrypt pre-1.x
#15968 assertion failure when fun tactic for abstract function isn't given argument Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16082 move * for adversary function outside { ... } Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16292 Side-conditions for the rnd rule in pHL should be proved under some precondition ckunz defect 3 EasyCrypt pre-1.x
#16456 allow expression, formula in cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16560 Non-relational 'bypr' for probabilistic Hoare statements ckunz enhancement 3 EasyCrypt pre-1.x
#16657 Pattern-matching on records Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16723 Subtyping for abstract modules and functors Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#16749 link between hoare bdhoare equiv Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#16763 Simplification should discriminate datatype constructors Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16789 Pattern matching should to some top-level delta-unfolding Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16918 selection tactical "all n" Pierre-Yves Strub enhancement 3 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
#15906 (local) opening of modules Pierre-Yves Strub enhancement 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
#15930 Clear all Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#16087 New view for apply: !a -> (a => false) Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#16622 Functor-level "lambdas" Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
#16746 Losslessness annotations Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#16885 Support for type annotations in let expressions Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x

Resolution: accepted (2 matches)

Ticket Summary Owner Type Priority Component Version
#15922 if tactic for bd_hoare doesn't work with precondition true Santiago Zanella-Béguelin defect 3 EasyCrypt pre-1.x
#15970 PG does not handle local lemmas properly. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
1 2 3 4 5
Note: See TracQuery for help on using queries.