Custom query (536 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (1 - 100 of 536)

1 2 3 4 5 6

Status: accepted (13 matches)

Ticket Summary Owner Type Priority Version Severity
#16113 <top> in printer Pierre-Yves Strub defect 2 pre-1.x minor
#17195 Swap with 2 args move as far down as possible Pierre-Yves Strub enhancement 3 pre-1.x minor
#17309 `rewrite /F` when F is a fixpoint should simplify selected occurence for head-iota reduction. Pierre-Yves Strub enhancement 3 pre-1.x minor
#17024 Pattern matching should try to infer memory and module parameters Pierre-Yves Strub enhancement 3 pre-1.x normal
#17034 Generalizing loop fusion Pierre-Yves Strub enhancement 3 pre-1.x normal
#17040 Syntactic sugar for nested if-then-else statements. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17042 Pattern matching in non-normal form. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17070 better error message when difference between goal and lemma is tiny Pierre-Yves Strub enhancement 3 pre-1.x normal
#17141 Wrong module type annotations accepted Pierre-Yves Strub defect 4 pre-1.x normal
#17250 off-by-one error in swap Pierre-Yves Strub defect 3 pre-1.x normal
#17392 problems with glob and delta and matching Pierre-Yves Strub defect 3 pre-1.x normal
#17408 issue warning or error message when defining theory whose name clashes with one treated specially by EasyCrypt Pierre-Yves Strub enhancement 3 pre-1.x normal
#17378 Proof of false using smt and Eprover. Pierre-Yves Strub defect 5 pre-1.x critical

Status: assigned (24 matches)

Ticket Summary Owner Type Priority Version Severity
#17343 (Optional) warning for old syntax Pierre-Yves Strub enhancement 1 pre-1.x trivial
#17345 Bad printing Pierre-Yves Strub defect 1 pre-1.x trivial
#17117 Warning when restrictions over an adversary are empty Benjamin Grégoire enhancement 2 pre-1.x minor
#17222 local clones do not disappear from the environment on section end Pierre-Yves Strub enhancement 3 pre-1.x minor
#17364 Internals: use Batteries maps instead of Why3 ones. Pierre-Yves Strub enhancement 1 pre-1.x minor
#17181 slow rewriting for large expressions Pierre-Yves Strub defect 3 pre-1.x normal
#17194 anomaly: EcHiGoal.LowApply.NoInstance (in byequiv) Benjamin Grégoire defect 3 pre-1.x normal
#17207 Applicative view Pierre-Yves Strub enhancement 3 pre-1.x normal
#17240 Syntactic sugar for proc. that reduces to a call to an external proc. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17253 EasyCrypt should fail gracefully when applying a tactic on a solved goal. Pierre-Yves Strub defect 2 pre-1.x normal
#17255 Missing unification in `clone...with...` Pierre-Yves Strub enhancement 3 pre-1.x normal
#17256 apply/rewrite should work modulo zeta-reduction. Pierre-Yves Strub defect 3 pre-1.x normal
#17261 `rewrite -/(f _)` should not match its own unfoldings. Pierre-Yves Strub defect 3 pre-1.x normal
#17262 Add the possibility to add rewrite hints to rewrite hint databases. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17263 Multiple incompleteness in `apply` Pierre-Yves Strub defect 3 pre-1.x normal
#17264 Add the possibility to clear lemmas when closing a theory. Pierre-Yves Strub defect 2 pre-1.x normal
#17265 `goal` vernacular command Pierre-Yves Strub defect 3 pre-1.x normal
#17268 Add a tactical that fails when no progress is done. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17271 Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn` Pierre-Yves Strub enhancement 3 pre-1.x normal
#17319 Anomaly triggered by `smt` defect 3 pre-1.x normal
#17334 this message need more information: cannot infer all placeholders Pierre-Yves Strub enhancement 3 pre-1.x normal
#17335 the formula contains free type variables Pierre-Yves Strub enhancement 3 pre-1.x normal
#17347 Search with notations is broken. Pierre-Yves Strub defect 2 pre-1.x normal
#17409 Termination checker failure defect 3 pre-1.x normal

Status: closed (63 matches)

Ticket Summary Owner Type Priority Version Severity
#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
#15786 Swap with call to the adversary defect 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
#15827 memory restriction for adversary does not take inner modules into account Benjamin Grégoire defect 3 pre-1.x
#15842 Bug in lambda translation Benjamin Grégoire defect 3 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
#15881 Complete path for local variable in printer Pierre-Yves Strub defect 3 pre-1.x
#15891 Instantiating axioms and sub-theories when cloning theories Pierre-Yves Strub enhancement 4 pre-1.x
#15893 Call in adversary call is not working properly Benjamin Grégoire defect 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
#15919 [case] tactic for bd_hoare is useless Benjamin Grégoire defect 3 pre-1.x
#15920 [conseq (_ : pre => _)] tactic for bd_hoare doesn't work Santiago Zanella-Béguelin defect 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
#15974 The following example generates an anomaly Benjamin Grégoire defect 3 pre-1.x
#15981 "delta cpEq" causes an untypable goal to be produced Benjamin Grégoire defect 3 pre-1.x
#15982 Printer bug for partially applied infix operators in prefix form Benjamin Grégoire defect 3 pre-1.x
#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
#16253 Non-local modules and abstract restrictions. defect 3 pre-1.x
#16292 Side-conditions for the rnd rule in pHL should be proved under some precondition ckunz defect 3 pre-1.x
#16362 Assertion failure when cloning a theory with let expressions Benjamin Grégoire defect 3 pre-1.x
#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
#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
#16732 Problem with functor aliases when outermost module is a parameter Benjamin Grégoire defect 3 pre-1.x
#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
#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
#15612 require Theory issues misleading "added" messages Pierre-Yves Strub defect 1 pre-1.x trivial
#15916 Extraneous internal memory identifier "hr" in output Pierre-Yves Strub defect 2 pre-1.x trivial
#15999 Pretty printer add too much scoping annotations. Pierre-Yves Strub defect 2 pre-1.x trivial
#16117 Fail to pose an arbitrary lambda Pierre-Yves Strub defect 2 pre-1.x trivial
#16504 Parse error on complex arguments to functions in probability statements Pierre-Yves Strub defect 2 pre-1.x trivial
#17007 Inconsistent syntax for closing sections/theories enhancement 2 pre-1.x trivial
#17033 Some program logic tactics that modify the precondition use bad associativity Pierre-Yves Strub enhancement 3 pre-1.x trivial
#17060 pretty printer still using "lambda" instead of "fun" defect 3 pre-1.x trivial
#17071 Error message for [expect] <default> enhancement 1 pre-1.x trivial
#17104 Make (<>) accessible in prefix form enhancement 1 pre-1.x trivial
#17115 [exfalso] tactic for ambient logic enhancement 3 pre-1.x trivial
#17121 Make Option.witness accessible at top level enhancement 3 pre-1.x trivial
#17185 Anomalies should give rise to a "This is a bug, please report."-type message. Pierre-Yves Strub enhancement 1 pre-1.x trivial
#17272 Wrong name defect 3 pre-1.x trivial
#17321 `case @[ambient]` needs its syntax unified with that of ambient `case` Pierre-Yves Strub enhancement 3 pre-1.x trivial
#15815 Search path for theories should include path of currently active file Pierre-Yves Strub defect 2 pre-1.x minor
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.