Custom query (519 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (301 - 400 of 519)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Version Severity
#17389 inline does not inline under match statement 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
#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
#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
#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
#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
#17171 mode similar to nocheck that tries smt calls and just prints the locations for the failing calls Pierre-Yves Strub enhancement 3 pre-1.x normal
#17173 alternative to "require A; clone export A as B" that does not add A to SMT context enhancement 3 pre-1.x normal
#17176 [print] should display types even on fixpoints Pierre-Yves Strub enhancement 3 pre-1.x normal
#17179 `done` should close goals with a direct contradiction in its env. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17185 Anomalies should give rise to a "This is a bug, please report."-type message. Pierre-Yves Strub enhancement 1 pre-1.x trivial
#17189 Syntax for referring to *local* variables by their long name Pierre-Yves Strub enhancement 3 pre-1.x normal
#17196 Vernacular command for dumping env. as a Why3 task. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17201 `x-y` and `x + -y` should be convertible 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.