Custom query (529 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (301 - 400 of 529)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Version Severity
#17387 no error message for match Pierre-Yves Strub defect 3 pre-1.x normal
#17389 inline does not inline under match statement defect 3 pre-1.x normal
#17391 case works with tuple corresponding to glob M, but not with glob M Pierre-Yves Strub defect 3 pre-1.x normal
#17393 Cloning polymorphic datatypes does not allow case analysis defect 3 pre-1.x normal
#17394 anomaly on some smt calls Pierre-Yves Strub defect 3 pre-1.x normal
#17398 problem with new eco facility Pierre-Yves Strub defect 3 pre-1.x normal
#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 pre-1.x normal
#17401 Generalizations may perform freeness checks in the wrong context defect 3 pre-1.x normal
#15106 Consider probability quantities as real-valued expressions enhancement 2 pre-1.x normal
#15520 request for more loop manipulation tactics Pierre-Yves Strub enhancement 3 pre-1.x normal
#15762 Tactic to transform a tuple equality into a conjonction Pierre-Yves Strub enhancement 3 pre-1.x
#15779 Inference during apply Pierre-Yves Strub enhancement 3 pre-1.x
#15808 Declaring/defining mixfix operators, using them when not in scope Pierre-Yves Strub enhancement 3 pre-1.x
#15809 Parsing/Printing scope for operator overloading "(x op y)%Scope" Pierre-Yves Strub enhancement 3 pre-1.x
#15817 Lighten EC syntax by removing the clumsy "<:" && "&" notations for modules / memories introductions / applications Pierre-Yves Strub enhancement 2 pre-1.x
#15849 Ignoring proof that are already done in a file Pierre-Yves Strub enhancement 3 pre-1.x
#15854 Allow sequences of variable declarations in procedure definitions Pierre-Yves Strub enhancement 3 pre-1.x
#15859 Omit path when it can be inferred from context Pierre-Yves Strub enhancement 3 pre-1.x
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 pre-1.x
#15879 While one sided ckunz enhancement 3 pre-1.x
#15880 Constant propagation with module variable Pierre-Yves Strub enhancement 3 pre-1.x
#15891 Instantiating axioms and sub-theories when cloning theories Pierre-Yves Strub enhancement 4 pre-1.x
#15906 (local) opening of modules Pierre-Yves Strub enhancement 2 pre-1.x
#15907 clone import and clone export Pierre-Yves Strub enhancement 3 pre-1.x
#15912 Be able to inline only one side after an equiv Pierre-Yves Strub enhancement 2 pre-1.x
#15917 Proving "a = b => f a = f b" should not require a call to SMT Pierre-Yves Strub enhancement 3 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 pre-1.x
#15921 A strongest post-condition tactic [sp n m], like in trunk ckunz enhancement 3 pre-1.x
#15930 Clear all Pierre-Yves Strub enhancement 2 pre-1.x
#15949 Improve kill error message Pierre-Yves Strub enhancement 2 pre-1.x minor
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 pre-1.x major
#16055 confusion of x{1} and x{2} with x in cut Pierre-Yves Strub enhancement 3 pre-1.x normal
#16058 Syntax f.x in equiv precondition for fonction argument enhancement 3 pre-1.x blocker
#16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 pre-1.x normal
#16082 move * for adversary function outside { ... } Pierre-Yves Strub enhancement 3 pre-1.x
#16087 New view for apply: !a -> (a => false) Pierre-Yves Strub enhancement 2 pre-1.x
#16104 naming issues enhancement 3 pre-1.x blocker
#16416 FEL completeness - initialization Benjamin Grégoire enhancement 3 pre-1.x normal
#16456 allow expression, formula in cloning Pierre-Yves Strub enhancement 3 pre-1.x
#16560 Non-relational 'bypr' for probabilistic Hoare statements ckunz enhancement 3 pre-1.x
#16622 Functor-level "lambdas" Benjamin Grégoire enhancement 2 pre-1.x
#16628 making nested sections work enhancement 3 pre-1.x normal
#16629 cloning within sections Pierre-Yves Strub enhancement 3 pre-1.x normal
#16648 Make notations and tactics on distributions and functions a bit more uniform. enhancement 3 pre-1.x normal
#16657 Pattern-matching on records Pierre-Yves Strub enhancement 3 pre-1.x
#16723 Subtyping for abstract modules and functors Benjamin Grégoire enhancement 3 pre-1.x
#16725 Intro pattern for substitution Pierre-Yves Strub enhancement 3 pre-1.x normal
#16737 "declare op" Pierre-Yves Strub enhancement 3 pre-1.x normal
#16746 Losslessness annotations Pierre-Yves Strub enhancement 2 pre-1.x
#16749 link between hoare bdhoare equiv Benjamin Grégoire enhancement 3 pre-1.x
#16763 Simplification should discriminate datatype constructors Pierre-Yves Strub enhancement 3 pre-1.x
#16780 Change the test script so the test suites can be run in weak check mode Pierre-Yves Strub enhancement 3 pre-1.x
#16786 Nicer treatment of datatype constructors Pierre-Yves Strub enhancement 3 pre-1.x normal
#16789 Pattern matching should to some top-level delta-unfolding Pierre-Yves Strub enhancement 3 pre-1.x
#16885 Support for type annotations in let expressions Pierre-Yves Strub enhancement 1 pre-1.x
#16918 selection tactical "all n" Pierre-Yves Strub enhancement 3 pre-1.x
#16963 op/pred nosmt ... Pierre-Yves Strub enhancement 3 pre-1.x normal
#16964 Warn when a variable is used before being initialized Pierre-Yves Strub enhancement 3 pre-1.x normal
#17005 Higher-order pattern matching enhancement 3 pre-1.x normal
#17007 Inconsistent syntax for closing sections/theories enhancement 2 pre-1.x trivial
#17016 Make elim and case work on tuples and records. Retire the special lemmas Pierre-Yves Strub enhancement 3 pre-1.x normal
#17033 Some program logic tactics that modify the precondition use bad associativity Pierre-Yves Strub enhancement 3 pre-1.x trivial
#17046 possible tactic renaming: [proc *] -> [eager proc *] Benjamin Grégoire enhancement 3 pre-1.x normal
#17057 Add the possibility to rule out the prover filtering mecanism from the command line. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17059 Negative line selectors in program logic tactics Pierre-Yves Strub enhancement 3 pre-1.x normal
#17066 Better error message when operator selection failed. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17067 Syntax for chained case analysis of the top-assumption Pierre-Yves Strub enhancement 3 pre-1.x normal
#17069 Improve error messages of the (P?R)HL tactics Pierre-Yves Strub enhancement 3 pre-1.x normal
#17071 Error message for [expect] <default> enhancement 1 pre-1.x trivial
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 pre-1.x minor
#17075 [sp] should fail when given code positions that cannot be reached Pierre-Yves Strub enhancement 3 pre-1.x normal
#17082 SMT tactic should be interruptable. Pierre-Yves Strub enhancement 4 pre-1.x normal
#17083 Missing eta-reduction in conversion Benjamin Grégoire enhancement 3 pre-1.x normal
#17084 syntax for non-flat proof-terms Pierre-Yves Strub enhancement 3 pre-1.x normal
#17087 [conseq*] should be the default behaviour of [conseq] Pierre-Yves Strub enhancement 4 pre-1.x normal
#17091 [rewrite] should head-reduce created b-redexes Pierre-Yves Strub enhancement 3 pre-1.x minor
#17092 Chaining [apply] Pierre-Yves Strub enhancement 3 pre-1.x minor
#17093 Add the possibility to declare several operators/predicates in 1 command. Pierre-Yves Strub enhancement 2 pre-1.x minor
#17096 Unfolding should work even in the presence of several matching operators. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17099 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 3 pre-1.x normal
#17100 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 3 pre-1.x normal
#17104 Make (<>) accessible in prefix form enhancement 1 pre-1.x trivial
#17106 Unification should work modulo delta-unfolding / simplification. enhancement 3 pre-1.x normal
#17108 require clone enhancement 3 pre-1.x normal
#17115 [exfalso] tactic for ambient logic enhancement 3 pre-1.x trivial
#17118 Add the ability to print the axioms of the environment enhancement 3 pre-1.x normal
#17119 Give the ability to print subgoals Pierre-Yves Strub enhancement 3 pre-1.x normal
#17121 Make Option.witness accessible at top level enhancement 3 pre-1.x trivial
#17126 Command and command line option for global timeout multiplier. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17130 "alias i" works only on random instruction. Benjamin Grégoire enhancement 3 pre-1.x normal
#17136 variant of seq to deal with large preconditions enhancement 3 pre-1.x normal
#17137 More tactical about goal selections Pierre-Yves Strub enhancement 3 pre-1.x normal
#17139 Multiple require at once. Pierre-Yves Strub enhancement 3 pre-1.x minor
#17151 Abstract theories Pierre-Yves Strub enhancement 3 pre-1.x normal
#17158 "<-" for predicates when cloning Pierre-Yves Strub enhancement 3 pre-1.x normal
#17159 expect should support goal selection Pierre-Yves Strub enhancement 3 pre-1.x normal
#17165 not-to-be-proved lemmas Pierre-Yves Strub enhancement 3 pre-1.x normal
#17166 missing syntax for proving all axioms of a theory, its subtheories, etc., when cloning Pierre-Yves Strub enhancement 3 pre-1.x normal
#17167 Better localization of errors when typing a proof-term Pierre-Yves Strub enhancement 3 pre-1.x normal
#17170 Introduce theory for product distribution Pierre-Yves Strub enhancement 3 pre-1.x normal
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.