Custom query (541 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (401 - 500 of 541)

1 2 3 4 5 6

Status: closed (52 matches)

Ticket Summary Owner Type Priority Component Version
#15106 Consider probability quantities as real-valued expressions enhancement 2 EasyCrypt pre-1.x
#15786 Swap with call to the adversary defect 3 EasyCrypt pre-1.x
#16058 Syntax f.x in equiv precondition for fonction argument enhancement 3 EasyCrypt pre-1.x
#16104 naming issues enhancement 3 EasyCrypt pre-1.x
#16229 Substitution issue when quantified module variables have the same name as an existing module defect 3 EasyCrypt pre-1.x
#16253 Non-local modules and abstract restrictions. defect 3 EasyCrypt pre-1.x
#16374 Visual weak-check indicator enhancement 1 ProofGeneral pre-1.x
#16468 try fails to catch some call-related exceptions defect 3 EasyCrypt pre-1.x
#16628 making nested sections work enhancement 3 EasyCrypt pre-1.x
#17005 Higher-order pattern matching enhancement 3 EasyCrypt pre-1.x
#17007 Inconsistent syntax for closing sections/theories enhancement 2 EasyCrypt pre-1.x
#17047 pretty printing of module type uses old notation for "*" defect 3 EasyCrypt pre-1.x
#17049 "restart scripting" not working in ProofGeneral defect 2 ProofGeneral pre-1.x
#17051 Pretty-printing regression defect 3 EasyCrypt pre-1.x
#17054 Finiteness of product of finite types enhancement 3 Libraries pre-1.x
#17055 Lemma linking eq_except and in_dom in FMap enhancement 3 Libraries pre-1.x
#17060 pretty printer still using "lambda" instead of "fun" defect 3 EasyCrypt pre-1.x
#17061 when arguments to seq are too big, anomaly rather than error message defect 3 EasyCrypt pre-1.x
#17095 anomaly raised by invariant form of [call upto] defect 3 EasyCrypt pre-1.x
#17104 Make (<>) accessible in prefix form enhancement 1 EasyCrypt pre-1.x
#17106 Unification should work modulo delta-unfolding / simplification. enhancement 3 EasyCrypt pre-1.x
#17107 Potential mismatch between spec and lemma versions of the "pHL + HL => pHL" variant of [conseq] defect 3 EasyCrypt pre-1.x
#17108 require clone enhancement 3 EasyCrypt pre-1.x
#17115 [exfalso] tactic for ambient logic enhancement 3 EasyCrypt pre-1.x
#17118 Add the ability to print the axioms of the environment enhancement 3 EasyCrypt pre-1.x
#17121 Make Option.witness accessible at top level enhancement 3 EasyCrypt pre-1.x
#17154 anomaly: EcPV.MemoryClash defect 3 EasyCrypt pre-1.x
#17173 alternative to "require A; clone export A as B" that does not add A to SMT context enhancement 3 EasyCrypt pre-1.x
#17174 Return of the memory explosion defect 3 EasyCrypt pre-1.x
#17188 Error with smt : lazy defect 3 EasyCrypt pre-1.x
#17216 All test suites should include abstract theory files (*.eca) defect 3 Internals pre-1.x
#17232 weirdness involving redefining (=) or defining (<>) enhancement 3 EasyCrypt pre-1.x
#17236 error with rewriting occurrence of -1 when only one matching occurrence defect 3 EasyCrypt pre-1.x
#17254 print produces misleading results on partially applied functors defect 3 EasyCrypt pre-1.x
#17272 Wrong name defect 3 EasyCrypt pre-1.x
#17273 `alias` failures look like uncaught exceptions defect 3 EasyCrypt pre-1.x
#17289 Missing dependencies in OPAM package defect 3 EasyCrypt pre-1.x
#17292 anomaly on application of a `<=>` lemma to a `=` goal defect 3 EasyCrypt pre-1.x
#17296 Some program tactics (`rnd`) generate invalid formulas when Distr is not loaded defect 3 EasyCrypt pre-1.x
#17299 Transitivity using an equiv enhancement 3 EasyCrypt phl
#17315 [print] on notations is not very useful defect 3 EasyCrypt pre-1.x
#17328 `_` intro-pattern should only check if the clear is possible once the rest of the intro-pattern has been processed enhancement 3 EasyCrypt pre-1.x
#17350 witness not in apRHL defect 3 EasyCrypt pre-1.x
#17352 Question about run easycrypt task 3 EasyCrypt pre-1.x
#17359 `rewrite ?lem` should fail (hard) if `lem` does not exist in scope enhancement 3 EasyCrypt pre-1.x
#17362 wildcard syntax for SMT provers in prover [...] enhancement 3 EasyCrypt pre-1.x
#17369 imprecise pretty printing with functor application defect 2 EasyCrypt pre-1.x
#17373 introduction pattern bug somehow related to SmtMap defect 3 EasyCrypt pre-1.x
#17379 Proving unreasonable/false lemmas through Alt-Ergo defect 5 EasyCrypt pre-1.x
#17381 Possible bug: no matching operator even when available defect 2 EasyCrypt pre-1.x
#17389 inline does not inline under match statement defect 3 EasyCrypt pre-1.x
#17393 Cloning polymorphic datatypes does not allow case analysis defect 3 EasyCrypt pre-1.x

Status: new (48 matches)

Ticket Summary Owner Type Priority Component Version
#17002 Better section && cloning support Pierre-Yves Strub task 3 EasyCrypt pre-1.x
#17037 Poor error message for module restriction example Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17077 No more direct access to stdlib paths Pierre-Yves Strub defect 4 Internals pre-1.x
#17082 SMT tactic should be interruptable. Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#17085 Generic Notations Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17088 `case !a` should reduce to proving `a` Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#16103 scoping issue with theories enhancement 3 EasyCrypt pre-1.x
#16648 Make notations and tactics on distributions and functions a bit more uniform. enhancement 3 EasyCrypt pre-1.x
#16912 Lifting the "collection update" statements to tuples enhancement 1 EasyCrypt pre-1.x
#16987 Move facts from precondition to context enhancement 3 EasyCrypt pre-1.x
#17022 Pattern-matching on variables in judgments and probability expressions enhancement 3 EasyCrypt pre-1.x
#17036 Instantiating abstract modules: warnings and interactive justification enhancement 1 EasyCrypt pre-1.x
#17045 Rewriting procedures in probability expressions directly from an equivalence enhancement 1 EasyCrypt pre-1.x
#17086 Generalize [rewrite Pr] enhancement 3 EasyCrypt pre-1.x
#17090 Selecting procedure(s) to [inline] by position enhancement 2 EasyCrypt pre-1.x
#17105 [transitivity] for phoare and hoare enhancement 3 EasyCrypt pre-1.x
#17113 Decide what to do on rewrite with defined head symbols enhancement 3 EasyCrypt pre-1.x
#17136 variant of seq to deal with large preconditions enhancement 3 EasyCrypt pre-1.x
#17140 Pattern matching should make use of simplification rules. enhancement 3 EasyCrypt pre-1.x
#17149 Expand glob A for concrete module enhancement 3 EasyCrypt pre-1.x
#17156 New vernacular command: `print axiom` enhancement 3 EasyCrypt pre-1.x
#17163 Check that `phoare` tactics are forcing the input bounds to be in [0..1]. task 4 EasyCrypt pre-1.x
#17164 behavior of -check-all enhancement 3 EasyCrypt pre-1.x
#17169 Anonymous functor arguments: passing procedures to functors directly enhancement 3 EasyCrypt pre-1.x
#17175 Direct intro on negative goals enhancement 3 EasyCrypt pre-1.x
#17183 Variant of `sim` that works modulo inlining. enhancement 1 EasyCrypt pre-1.x
#17192 Problem with `glob` and type inference defect 3 EasyCrypt pre-1.x
#17197 Asserts in equivalence proofs enhancement 3 EasyCrypt pre-1.x
#17202 Add seq* tactic enhancement 3 EasyCrypt pre-1.x
#17210 Pattern-matching for pairs in operator arguments enhancement 3 EasyCrypt pre-1.x
#17215 Issues with module typing when functor parameters are themselves functors defect 3 EasyCrypt pre-1.x
#17217 need better error message when attempting to apply lemma to goal that isn't a judgment enhancement 3 EasyCrypt pre-1.x
#17218 proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate enhancement 3 EasyCrypt pre-1.x
#17225 Explore reproducible smt calls enhancement 3 EasyCrypt pre-1.x
#17239 Mutual inductive types. enhancement 3 EasyCrypt pre-1.x
#17245 Formula manipulation commands (for `conseq` and `seq`) enhancement 3 EasyCrypt pre-1.x
#17246 `rewrite`, apply, ... in contracts defect 3 EasyCrypt pre-1.x
#17251 print Self enhancement 3 EasyCrypt pre-1.x
#17257 `/=` is too weak. defect 3 EasyCrypt pre-1.x
#17259 Theory of distribution (iso)morphisms task 3 Libraries pre-1.x
#17267 `auto` with `call` enhancement 3 EasyCrypt pre-1.x
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` enhancement 3 EasyCrypt pre-1.x
#17281 Several problems with `apply` in program logics enhancement 3 EasyCrypt pre-1.x
#17282 call should not work task 3 EasyCrypt phl
#17283 pattern matching complexity problem defect 3 EasyCrypt pre-1.x
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. enhancement 3 EasyCrypt pre-1.x
#17286 pRHL `apply` should have a framing variant enhancement 3 EasyCrypt pre-1.x
#17287 Program transformation tactics should not `anomaly` without a side in pRHL defect 3 EasyCrypt pre-1.x
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.