Custom query (519 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (1 - 100 of 519)

1 2 3 4 5 6

Status: accepted (12 matches)

Ticket Summary Owner Type Priority Version Severity
#17070 better error message when difference between goal and lemma is tiny Pierre-Yves Strub enhancement 3 pre-1.x normal
#17034 Generalizing loop fusion Pierre-Yves Strub enhancement 3 pre-1.x normal
#17250 off-by-one error in swap Pierre-Yves Strub defect 3 pre-1.x normal
#17042 Pattern matching in non-normal form. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17024 Pattern matching should try to infer memory and module parameters Pierre-Yves Strub enhancement 3 pre-1.x normal
#17392 problems with glob and delta and matching Pierre-Yves Strub defect 3 pre-1.x normal
#17378 Proof of false using smt and Eprover. Pierre-Yves Strub defect 5 pre-1.x critical
#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
#17195 Swap with 2 args move as far down as possible Pierre-Yves Strub enhancement 3 pre-1.x minor
#17040 Syntactic sugar for nested if-then-else statements. Pierre-Yves Strub enhancement 3 pre-1.x normal
#16113 <top> in printer Pierre-Yves Strub defect 2 pre-1.x minor
#17141 Wrong module type annotations accepted Pierre-Yves Strub defect 4 pre-1.x normal

Status: assigned (27 matches)

Ticket Summary Owner Type Priority Version Severity
#17268 Add a tactical that fails when no progress is done. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17269 Add notations for >/>= Pierre-Yves Strub enhancement 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
#17264 Add the possibility to clear lemmas when closing a theory. Pierre-Yves Strub defect 2 pre-1.x normal
#17194 anomaly: EcHiGoal.LowApply.NoInstance (in byequiv) Benjamin Grégoire defect 3 pre-1.x normal
#17319 Anomaly triggered by `smt` defect 3 pre-1.x normal
#17207 Applicative view 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
#17345 Bad printing Pierre-Yves Strub defect 1 pre-1.x trivial
#17270 `done` should close a goal when `false` is a local hyp. 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
#17265 `goal` vernacular command Pierre-Yves Strub defect 3 pre-1.x normal
#17364 Internals: use Batteries maps instead of Why3 ones. Pierre-Yves Strub enhancement 1 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
#17255 Missing unification in `clone...with...` Pierre-Yves Strub enhancement 3 pre-1.x normal
#17263 Multiple incompleteness in `apply` Pierre-Yves Strub defect 3 pre-1.x normal
#17343 (Optional) warning for old syntax Pierre-Yves Strub enhancement 1 pre-1.x trivial
#17271 Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn` Pierre-Yves Strub enhancement 3 pre-1.x normal
#17308 `rewrite !(A,B)` loops when `B` is not known about 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
#17347 Search with notations is broken. Pierre-Yves Strub defect 2 pre-1.x normal
#17181 slow rewriting for large expressions Pierre-Yves Strub defect 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
#17335 the formula contains free type variables Pierre-Yves Strub enhancement 3 pre-1.x normal
#17334 this message need more information: cannot infer all placeholders Pierre-Yves Strub enhancement 3 pre-1.x normal
#17310 Top-level command to print various databases (exact, rewrite, ...) Pierre-Yves Strub defect 2 pre-1.x minor
#17117 Warning when restrictions over an adversary are empty Benjamin Grégoire enhancement 2 pre-1.x minor

Status: closed (61 matches)

Ticket Summary Owner Type Priority Version Severity
#17009 1.x error messages Pierre-Yves Strub defect 3 pre-1.x normal
#17151 Abstract theories Pierre-Yves Strub enhancement 3 pre-1.x normal
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 pre-1.x
#17118 Add the ability to print the axioms of the environment enhancement 3 pre-1.x normal
#17093 Add the possibility to declare several operators/predicates in 1 command. Pierre-Yves Strub enhancement 2 pre-1.x minor
#17057 Add the possibility to rule out the prover filtering mecanism from the command line. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17249 `AlgTactic` && `Ring` should agree on their axioms. Pierre-Yves Strub enhancement 2 pre-1.x normal
#17273 `alias` failures look like uncaught exceptions defect 3 pre-1.x minor
#17130 "alias i" works only on random instruction. Benjamin Grégoire enhancement 3 pre-1.x normal
#16456 allow expression, formula in cloning Pierre-Yves Strub enhancement 3 pre-1.x
#17234 Allow omission of a procedure's return type when it can be inferred Pierre-Yves Strub enhancement 3 pre-1.x normal
#15854 Allow sequences of variable declarations in procedure definitions Pierre-Yves Strub enhancement 3 pre-1.x
#17124 allows to specify timeout only for smt. Pierre-Yves Strub defect 3 pre-1.x normal
#17035 Alt-Ergo succeeds on false obligations in weird circumstances Pierre-Yves Strub defect 4 pre-1.x critical
#17173 alternative to "require A; clone export A as B" that does not add A to SMT context enhancement 3 pre-1.x normal
#17372 "" and "!" semantic for smt 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
#16984 Anomaly due to inlining functions with tuple arguments Pierre-Yves Strub defect 3 pre-1.x major
#17339 `anomaly: EcLowGoal.InvalidProofTerm.` on `/>` Pierre-Yves Strub defect 4 pre-1.x major
#17154 anomaly: EcPV.MemoryClash defect 3 pre-1.x normal
#17180 anomaly: File "src/ecCoreFol.ml", line 1207, characters 19-25: Assertion failed Pierre-Yves Strub defect 3 pre-1.x normal
#17143 Anomaly (free type variables in conseq) Pierre-Yves Strub defect 3 pre-1.x normal
#17089 anomaly in [sim] Benjamin Grégoire defect 4 pre-1.x normal
#17292 anomaly on application of a `<=>` lemma to a `=` goal defect 3 pre-1.x normal
#17330 anomaly on `apply/contra` Pierre-Yves Strub defect 3 pre-1.x normal
#17394 anomaly on some smt calls Pierre-Yves Strub defect 3 pre-1.x normal
#17110 [anomaly] on using [call] with a lemma referring to the wrong procedure Pierre-Yves Strub defect 2 pre-1.x normal
#17095 anomaly raised by invariant form of [call upto] defect 3 pre-1.x normal
#17142 Anomaly (related to SMT and memories) Benjamin Grégoire defect 3 pre-1.x normal
#17320 anomaly when cloning theory with inductive predicate Pierre-Yves Strub defect 3 pre-1.x normal
#17101 [anomaly] when defining an operator over a concrete module's globals Pierre-Yves Strub defect 3 pre-1.x normal
#17135 anomaly when intro pattern has wrong form Pierre-Yves Strub defect 3 pre-1.x minor
#17187 anomaly when invalid memory is referenced -- should be proper error message Pierre-Yves Strub defect 3 pre-1.x normal
#17102 [anomaly] when pHL => pRHL variant of conseq is used with a bound different from [=1%r] Pierre-Yves Strub defect 3 pre-1.x normal
#17238 anomaly with auto-revert intro pattern Pierre-Yves Strub defect 3 pre-1.x normal
#16788 Another stack overflow during unification Pierre-Yves Strub defect 3 pre-1.x normal
#15877 Apply is not working when trying to use it to instantiate a lemma that is quantified on modules Pierre-Yves Strub defect 3 pre-1.x blocker
#17191 Assert failure Pierre-Yves Strub defect 3 pre-1.x normal
#17128 assert false in rnd. Benjamin Grégoire defect 3 pre-1.x normal
#15924 Assertion failed in otherwise provable goal Pierre-Yves Strub defect 3 pre-1.x normal
#15965 Assertion failure in EcEnv Pierre-Yves Strub defect 3 pre-1.x major
#16138 assertion failure when call tactic not given { ... } module restriction Benjamin Grégoire defect 3 pre-1.x normal
#16362 Assertion failure when cloning a theory with let expressions Benjamin Grégoire defect 3 pre-1.x
#15968 assertion failure when fun tactic for abstract function isn't given argument Benjamin Grégoire defect 3 pre-1.x normal
#15921 A strongest post-condition tactic [sp n m], like in trunk ckunz enhancement 3 pre-1.x
#16114 Bad error message Pierre-Yves Strub defect 2 pre-1.x minor
#17116 Bad error message for [swap] Pierre-Yves Strub defect 3 pre-1.x minor
#17146 Bad error message in combination choice/modules/section Pierre-Yves Strub defect 3 pre-1.x normal
#16002 bad error message when predicate is given polymorphic constant Pierre-Yves Strub defect 2 pre-1.x minor
#16067 bad error message when value is treated as function Pierre-Yves Strub defect 2 pre-1.x minor
#16102 bad error message when value of constant refers to module variable Pierre-Yves Strub defect 2 pre-1.x minor
#17044 Bad inlining when giving an argument of type unit to a procedure that expects no arguments Pierre-Yves Strub defect 3 pre-1.x major
#17162 Bad interaction between abstract theories and local modules Pierre-Yves Strub defect 4 pre-1.x normal
#16066 bad line number in error message when run in batch mode Pierre-Yves Strub defect 2 pre-1.x minor
#17123 Bad parsing on call (_: B, I) Pierre-Yves Strub defect 3 pre-1.x normal
#17097 Bad pretty-printing of lists. Pierre-Yves Strub defect 3 pre-1.x normal
#16727 bd_hoare should work on >=, rather than forcing us to swap arguments Benjamin Grégoire defect 3 pre-1.x minor
#15912 Be able to inline only one side after an equiv Pierre-Yves Strub enhancement 2 pre-1.x
#17376 behaviour of module type include in functor types Benjamin Grégoire enhancement 3 pre-1.x normal
#17066 Better error message when operator selection failed. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17332 Better localisation when a pattern cannot be infered 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.