Custom query (551 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (301 - 400 of 551)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Component Version
#17330 anomaly on `apply/contra` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17339 `anomaly: EcLowGoal.InvalidProofTerm.` on `/>` Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17350 witness not in apRHL defect 3 EasyCrypt pre-1.x
#17354 In cloning, `rename` should not be allowed to create unreachable/unparsable symbols Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17355 Pretty-printer sometimes forget to use the abbreviation Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17361 scoping problem with theory renaming Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17365 Proof of false using Ring and Reals. Pierre-Yves Strub defect 5 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
#17380 Internal "seq" of pHL tactics is unsound Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17381 Possible bug: no matching operator even when available defect 2 EasyCrypt pre-1.x
#17385 problem sending goal to SMT (involving inductive datatype and higher order function) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17387 no error message for match Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17389 inline does not inline under match statement defect 3 EasyCrypt pre-1.x
#17391 case works with tuple corresponding to glob M, but not with glob M Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17393 Cloning polymorphic datatypes does not allow case analysis defect 3 EasyCrypt pre-1.x
#17394 anomaly on some smt calls Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17398 problem with new eco facility Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17400 eco problem: .ec file that uses unchanged .ec file is rechecked even though nothing changed and eco files stable Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17401 Generalizations may perform freeness checks in the wrong context defect 3 EasyCrypt pre-1.x
#15106 Consider probability quantities as real-valued expressions enhancement 2 EasyCrypt pre-1.x
#15520 request for more loop manipulation tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15762 Tactic to transform a tuple equality into a conjonction Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15779 Inference during apply Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15808 Declaring/defining mixfix operators, using them when not in scope Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15809 Parsing/Printing scope for operator overloading "(x op y)%Scope" 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
#15849 Ignoring proof that are already done in a file Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15854 Allow sequences of variable declarations in procedure definitions Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15859 Omit path when it can be inferred from context Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 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
#15891 Instantiating axioms and sub-theories when cloning theories Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#15906 (local) opening of modules Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15907 clone import and clone export Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15912 Be able to inline only one side after an equiv Pierre-Yves Strub enhancement 2 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
#15930 Clear all Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15949 Improve kill error message Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 EasyCrypt pre-1.x
#16055 confusion of x{1} and x{2} with x in cut Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16058 Syntax f.x in equiv precondition for fonction argument enhancement 3 EasyCrypt pre-1.x
#16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#16082 move * for adversary function outside { ... } Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16087 New view for apply: !a -> (a => false) Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#16104 naming issues enhancement 3 EasyCrypt pre-1.x
#16374 Visual weak-check indicator enhancement 1 ProofGeneral pre-1.x
#16416 FEL completeness - initialization Benjamin Grégoire enhancement 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
#16622 Functor-level "lambdas" Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
#16628 making nested sections work enhancement 3 EasyCrypt pre-1.x
#16629 cloning within sections Pierre-Yves Strub 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
#16725 Intro pattern for substitution Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16737 "declare op" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16746 Losslessness annotations Pierre-Yves Strub enhancement 2 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
#16780 Change the test script so the test suites can be run in weak check mode Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16786 Nicer treatment of 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
#16885 Support for type annotations in let expressions Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#16918 selection tactical "all n" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16963 op/pred nosmt ... Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16964 Warn when a variable is used before being initialized Pierre-Yves Strub 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
#17016 Make elim and case work on tuples and records. Retire the special lemmas Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17033 Some program logic tactics that modify the precondition use bad associativity Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17046 possible tactic renaming: [proc *] -> [eager proc *] Benjamin Grégoire enhancement 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
#17057 Add the possibility to rule out the prover filtering mecanism from the command line. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17059 Negative line selectors in program logic tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17066 Better error message when operator selection failed. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17067 Syntax for chained case analysis of the top-assumption Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17069 Improve error messages of the (P?R)HL tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17071 Error message for [expect] <default> enhancement 1 EasyCrypt pre-1.x
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17075 [sp] should fail when given code positions that cannot be reached Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17083 Missing eta-reduction in conversion Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17084 syntax for non-flat proof-terms Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17087 [conseq*] should be the default behaviour of [conseq] Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#17091 [rewrite] should head-reduce created b-redexes Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17092 Chaining [apply] Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17093 Add the possibility to declare several operators/predicates in 1 command. Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17094 Refactoring: code for operators addition. Pierre-Yves Strub enhancement 3 Internals pre-1.x
#17096 Unfolding should work even in the presence of several matching operators. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17098 Add a search facility Pierre-Yves Strub enhancement 4 Documentation pre-1.x
#17099 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17100 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 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
#17108 require clone 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.