Custom query (514 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (401 - 500 of 514)

1 2 3 4 5 6

Status: closed (29 matches)

Ticket Summary Owner Type Priority Version Severity
#17107 Potential mismatch between spec and lemma versions of the "pHL + HL => pHL" variant of [conseq] defect 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
#17121 Make Option.witness accessible at top level enhancement 3 pre-1.x trivial
#17154 anomaly: EcPV.MemoryClash defect 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
#17174 Return of the memory explosion defect 3 pre-1.x normal
#17188 Error with smt : lazy defect 3 pre-1.x normal
#17232 weirdness involving redefining (=) or defining (<>) enhancement 3 pre-1.x normal
#17236 error with rewriting occurrence of -1 when only one matching occurrence defect 3 pre-1.x normal
#17254 print produces misleading results on partially applied functors defect 3 pre-1.x normal
#17272 Wrong name defect 3 pre-1.x trivial
#17273 `alias` failures look like uncaught exceptions defect 3 pre-1.x minor
#17289 Missing dependencies in OPAM package defect 3 pre-1.x normal
#17292 anomaly on application of a `<=>` lemma to a `=` goal defect 3 pre-1.x normal
#17296 Some program tactics (`rnd`) generate invalid formulas when Distr is not loaded defect 3 pre-1.x normal
#17299 Transitivity using an equiv enhancement 3 phl normal
#17315 [print] on notations is not very useful defect 3 pre-1.x normal
#17328 `_` intro-pattern should only check if the clear is possible once the rest of the intro-pattern has been processed enhancement 3 pre-1.x normal
#17350 witness not in apRHL defect 3 pre-1.x normal
#17352 Question about run easycrypt task 3 pre-1.x normal
#17359 `rewrite ?lem` should fail (hard) if `lem` does not exist in scope enhancement 3 pre-1.x normal
#17362 wildcard syntax for SMT provers in prover [...] enhancement 3 pre-1.x normal
#17369 imprecise pretty printing with functor application defect 2 pre-1.x normal
#17373 introduction pattern bug somehow related to SmtMap defect 3 pre-1.x normal
#17379 Proving unreasonable/false lemmas through Alt-Ergo defect 5 pre-1.x critical
#17381 Possible bug: no matching operator even when available defect 2 pre-1.x normal
#17389 inline does not inline under match statement defect 3 pre-1.x normal

Status: new (71 matches)

Ticket Summary Owner Type Priority Version Severity
#17002 Better section && cloning support Pierre-Yves Strub task 3 pre-1.x major
#17037 Poor error message for module restriction example Pierre-Yves Strub enhancement 2 pre-1.x minor
#17082 SMT tactic should be interruptable. Pierre-Yves Strub enhancement 4 pre-1.x normal
#17085 Generic Notations Pierre-Yves Strub enhancement 3 pre-1.x normal
#17088 `case !a` should reduce to proving `a` Pierre-Yves Strub enhancement 2 pre-1.x normal
#16103 scoping issue with theories enhancement 3 pre-1.x
#16648 Make notations and tactics on distributions and functions a bit more uniform. enhancement 3 pre-1.x normal
#16912 Lifting the "collection update" statements to tuples enhancement 1 pre-1.x normal
#16987 Move facts from precondition to context enhancement 3 pre-1.x normal
#17022 Pattern-matching on variables in judgments and probability expressions enhancement 3 pre-1.x normal
#17036 Instantiating abstract modules: warnings and interactive justification enhancement 1 pre-1.x normal
#17045 Rewriting procedures in probability expressions directly from an equivalence enhancement 1 pre-1.x normal
#17086 Generalize [rewrite Pr] enhancement 3 pre-1.x normal
#17090 Selecting procedure(s) to [inline] by position enhancement 2 pre-1.x normal
#17105 [transitivity] for phoare and hoare enhancement 3 pre-1.x normal
#17113 Decide what to do on rewrite with defined head symbols enhancement 3 pre-1.x normal
#17136 variant of seq to deal with large preconditions enhancement 3 pre-1.x normal
#17140 Pattern matching should make use of simplification rules. enhancement 3 pre-1.x normal
#17149 Expand glob A for concrete module enhancement 3 pre-1.x normal
#17156 New vernacular command: `print axiom` enhancement 3 pre-1.x normal
#17163 Check that `phoare` tactics are forcing the input bounds to be in [0..1]. task 4 pre-1.x major
#17164 behavior of -check-all enhancement 3 pre-1.x normal
#17169 Anonymous functor arguments: passing procedures to functors directly enhancement 3 pre-1.x normal
#17175 Direct intro on negative goals enhancement 3 pre-1.x normal
#17183 Variant of `sim` that works modulo inlining. enhancement 1 pre-1.x normal
#17192 Problem with `glob` and type inference defect 3 pre-1.x normal
#17197 Asserts in equivalence proofs enhancement 3 pre-1.x normal
#17202 Add seq* tactic enhancement 3 pre-1.x major
#17210 Pattern-matching for pairs in operator arguments enhancement 3 pre-1.x normal
#17215 Issues with module typing when functor parameters are themselves functors defect 3 pre-1.x normal
#17217 need better error message when attempting to apply lemma to goal that isn't a judgment enhancement 3 pre-1.x normal
#17218 proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate enhancement 3 pre-1.x normal
#17225 Explore reproducible smt calls enhancement 3 pre-1.x normal
#17239 Mutual inductive types. enhancement 3 pre-1.x normal
#17245 Formula manipulation commands (for `conseq` and `seq`) enhancement 3 pre-1.x normal
#17246 `rewrite`, apply, ... in contracts defect 3 pre-1.x normal
#17251 print Self enhancement 3 pre-1.x normal
#17257 `/=` is too weak. defect 3 pre-1.x normal
#17267 `auto` with `call` enhancement 3 pre-1.x normal
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` enhancement 3 pre-1.x normal
#17281 Several problems with `apply` in program logics enhancement 3 pre-1.x normal
#17282 call should not work task 3 phl normal
#17283 pattern matching complexity problem defect 3 pre-1.x normal
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. enhancement 3 pre-1.x normal
#17286 pRHL `apply` should have a framing variant enhancement 3 pre-1.x normal
#17287 Program transformation tactics should not `anomaly` without a side in pRHL defect 3 pre-1.x normal
#17288 EasyCrypt crashes when printing required abstract theory IterProc defect 3 pre-1.x normal
#17290 `n!->>` should work enhancement 3 pre-1.x normal
#17295 local ops enhancement 3 pre-1.x normal
#17297 Allow the optional use of undeclared variables in procedures enhancement 1 pre-1.x normal
#17298 Super rnd enhancement 4 phl blocker
#17301 Applicative view for `if then else` enhancement 3 pre-1.x normal
#17305 proc* in eager case needlessly assigns result of procedures returning unit to variables enhancement 3 pre-1.x normal
#17307 Coq style Locate enhancement 1 pre-1.x minor
#17311 `smt (@Self)` enhancement 3 pre-1.x normal
#17316 [smt (@Theory)] should force the use of axioms marked as `nosmt` defect 3 pre-1.x normal
#17317 `search` should work somewhat better with abbreviations enhancement 3 pre-1.x normal
#17322 use of side with HL version of while tactic should be syntax error defect 3 pre-1.x normal
#17325 syntax marking end of cloning realization enhancement 3 pre-1.x normal
#17337 substitutions should complain when substituting a locally defined variable enhancement 3 pre-1.x normal
#17340 cfold should support variables (and more general terms). enhancement 3 pre-1.x normal
#17341 for loops enhancement 3 pre-1.x normal
#17342 Better support for rewriting with equivalences enhancement 3 pre-1.x normal
#17344 Trees and polynomials enhancement 3 pre-1.x normal
#17346 have access to notation in ml defect 3 pre-1.x normal
#17348 Intro-pattern `|>` might transform a provable goal to a non-provable one defect 3 pre-1.x normal
#17349 call tactic for aequiv conclusions enhancement 3 pre-1.x normal
#17351 sp for aqeuiv goals enhancement 3 pre-1.x normal
#17353 `&&` could disappear from internal code, and be replaced by distinct splitting lemmas for `/\` enhancement 1 pre-1.x normal
#17356 Two-sided `rcondx` enhancement 1 pre-1.x normal
#17357 rnd tactic for aprhl 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.