Custom query (536 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (401 - 500 of 536)

1 2 3 4 5 6

Status: closed (48 matches)

Ticket Summary Owner Type Priority Component Version
#17324 |> ip expands predicates in conclusion Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17326 `+` intro-pattern may reorder assumptions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17327 Variants of `<*>` with preference Pierre-Yves Strub enhancement 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
#17329 EasyCrypt output (goals order e.g.) is not stable Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17330 anomaly on `apply/contra` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17331 Tactic arguments for the `exists` tactic should not be comma-separated Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17332 Better localisation when a pattern cannot be infered Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17333 We need a `pragma` to stop EasyCrypt from reducing `b => false` into `!b`. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17336 `inline` procedure selection by code position Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17338 misspelled pragmas are not reported Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17339 `anomaly: EcLowGoal.InvalidProofTerm.` on `/>` Pierre-Yves Strub defect 4 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
#17354 In cloning, `rename` should not be allowed to create unreachable/unparsable symbols Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17355 Pretty-printer sometimes forget to use the abbreviation Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17359 `rewrite ?lem` should fail (hard) if `lem` does not exist in scope enhancement 3 EasyCrypt pre-1.x
#17361 scoping problem with theory renaming Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17362 wildcard syntax for SMT provers in prover [...] enhancement 3 EasyCrypt pre-1.x
#17365 Proof of false using Ring and Reals. Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17369 imprecise pretty printing with functor application defect 2 EasyCrypt pre-1.x
#17371 new option for smt Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17372 "" and "!" semantic for smt Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17373 introduction pattern bug somehow related to SmtMap defect 3 EasyCrypt pre-1.x
#17375 `include` command for modules / module types Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17376 behaviour of module type include in functor types Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17377 characterization lemmas for <=> and \proper Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17379 Proving unreasonable/false lemmas through Alt-Ergo defect 5 EasyCrypt pre-1.x
#17380 Internal "seq" of pHL tactics is unsound Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17381 Possible bug: no matching operator even when available defect 2 EasyCrypt pre-1.x
#17387 no error message for match Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17389 inline does not inline under match statement defect 3 EasyCrypt pre-1.x
#17078 EasyCrypt should use big integers internally. Pierre-Yves Strub defect 3 Internals pre-1.x
#17080 `t_generalize_hyps` does not work when given a non-singleton list. Pierre-Yves Strub defect 4 Internals pre-1.x
#17094 Refactoring: code for operators addition. Pierre-Yves Strub enhancement 3 Internals pre-1.x
#17216 All test suites should include abstract theory files (*.eca) defect 3 Internals 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
#17079 Make the test-suite pass. Pierre-Yves Strub defect 5 Libraries pre-1.x
#15769 ProofGeneral issue with new EasyCrypt: undo step at EOF give Emacs type error Pierre-Yves Strub defect 3 ProofGeneral pre-1.x
#15852 Undo immediately after 'save.' does not work Pierre-Yves Strub defect 1 ProofGeneral pre-1.x
#15853 timeout and prover settings are not undone Pierre-Yves Strub defect 3 ProofGeneral pre-1.x
#16374 Visual weak-check indicator enhancement 1 ProofGeneral pre-1.x
#16663 Goal window should update on tactic failure... Pierre-Yves Strub defect 2 ProofGeneral pre-1.x
#17049 "restart scripting" not working in ProofGeneral defect 2 ProofGeneral pre-1.x
#17199 PG: Default weak-check mode indicator is invalid. Pierre-Yves Strub defect 2 ProofGeneral pre-1.x
#17213 Retracting/Resetting should cause easycrypt to reload the prelude Pierre-Yves Strub defect 3 ProofGeneral pre-1.x
#17266 Clear goal window when no more goals Pierre-Yves Strub enhancement 2 ProofGeneral pre-1.x

Status: new (52 matches)

Ticket Summary Owner Type Priority Component Version
#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
#17002 Better section && cloning support Pierre-Yves Strub task 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
#17037 Poor error message for module restriction example Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17045 Rewriting procedures in probability expressions directly from an equivalence enhancement 1 EasyCrypt 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
#17086 Generalize [rewrite Pr] enhancement 3 EasyCrypt pre-1.x
#17088 `case !a` should reduce to proving `a` Pierre-Yves Strub enhancement 2 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
#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
#17288 EasyCrypt crashes when printing required abstract theory IterProc defect 3 EasyCrypt pre-1.x
#17290 `n!->>` should work enhancement 3 EasyCrypt pre-1.x
#17295 local ops enhancement 3 EasyCrypt pre-1.x
#17297 Allow the optional use of undeclared variables in procedures enhancement 1 EasyCrypt pre-1.x
#17298 Super rnd enhancement 4 EasyCrypt phl
#17301 Applicative view for `if then else` enhancement 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.