Custom query (405 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (301 - 400 of 405)

1 2 3 4 5

Resolution: fixed (22 matches)

Ticket Summary Owner Type Priority Component Version
#16457 try tactic not catching case failure Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#16504 Parse error on complex arguments to functions in probability statements Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#16663 Goal window should update on tactic failure... Pierre-Yves Strub defect 2 ProofGeneral pre-1.x
#16773 "do! rewrite /op" loops Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17007 Inconsistent syntax for closing sections/theories enhancement 2 EasyCrypt pre-1.x
#17011 Pretty-printer in adding too much scoping annotation Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17026 EasyCrypt does not compile on Windows (win32 / cygwin) Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17049 "restart scripting" not working in ProofGeneral defect 2 ProofGeneral pre-1.x
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17093 Add the possibility to declare several operators/predicates in 1 command. Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17110 [anomaly] on using [call] with a lemma referring to the wrong procedure Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17199 PG: Default weak-check mode indicator is invalid. Pierre-Yves Strub defect 2 ProofGeneral pre-1.x
#17227 Procedures with unit return type should be allowed to return `tt' Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17249 `AlgTactic` && `Ring` should agree on their axioms. Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17266 Clear goal window when no more goals Pierre-Yves Strub enhancement 2 ProofGeneral pre-1.x
#17369 imprecise pretty printing with functor application defect 2 EasyCrypt pre-1.x
#15612 require Theory issues misleading "added" messages Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17071 Error message for [expect] <default> enhancement 1 EasyCrypt pre-1.x
#17185 Anomalies should give rise to a "This is a bug, please report."-type message. Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17204 Syntax for ignoring the return value of a procedure call Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17294 `Self` (and `Top`) should be allowed in module restrictions Pierre-Yves Strub defect 1 EasyCrypt pre-1.x

Resolution: invalid (15 matches)

Ticket Summary Owner Type Priority Component Version
#17155 Fix stdlib w.r.t. why3 import Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#15814 call tactic accepts variable defined in left game ({1}) defined for right game Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16253 Non-local modules and abstract restrictions. defect 3 EasyCrypt pre-1.x
#16512 Bug in pose Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17033 Some program logic tactics that modify the precondition use bad associativity Pierre-Yves Strub 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
#17134 is_lossless F(M).f generate a parse error. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17191 Assert failure Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17236 error with rewriting occurrence of -1 when only one matching occurrence defect 3 EasyCrypt pre-1.x
#17272 Wrong name defect 3 EasyCrypt pre-1.x
#17289 Missing dependencies in OPAM package defect 3 EasyCrypt pre-1.x
#15915 conjunctive introduction pattern does not split <=> Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#15999 Pretty printer add too much scoping annotations. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#16459 elim failing on pattern-matching let expressions Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#16460 elim fails on let statements that can be simplified away Pierre-Yves Strub defect 2 EasyCrypt pre-1.x

Resolution: wontfix (10 matches)

Ticket Summary Owner Type Priority Component Version
#15884 Repeat tactic broken Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17046 possible tactic renaming: [proc *] -> [eager proc *] Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17115 [exfalso] tactic for ambient logic enhancement 3 EasyCrypt pre-1.x
#17121 Make Option.witness accessible at top level enhancement 3 EasyCrypt pre-1.x
#17232 weirdness involving redefining (=) or defining (<>) enhancement 3 EasyCrypt pre-1.x
#17350 witness not in apRHL 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
#15852 Undo immediately after 'save.' does not work Pierre-Yves Strub defect 1 ProofGeneral pre-1.x
#16374 Visual weak-check indicator enhancement 1 ProofGeneral pre-1.x
#17104 Make (<>) accessible in prefix form enhancement 1 EasyCrypt pre-1.x

Resolution: duplicate (15 matches)

Ticket Summary Owner Type Priority Component Version
#15520 request for more loop manipulation tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16058 Syntax f.x in equiv precondition for fonction argument 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
#16628 making nested sections work enhancement 3 EasyCrypt pre-1.x
#16629 cloning within sections Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16737 "declare op" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17099 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17108 require clone enhancement 3 EasyCrypt pre-1.x
#17118 Add the ability to print the axioms of the environment enhancement 3 EasyCrypt pre-1.x
#17133 seq for phoare do not check the type of the arguments. Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17146 Bad error message in combination choice/modules/section Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17154 anomaly: EcPV.MemoryClash 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
#17332 Better localisation when a pattern cannot be infered Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x

Resolution: worksforme (5 matches)

Ticket Summary Owner Type Priority Component Version
#17052 Parse error on (**) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17095 anomaly raised by invariant form of [call upto] 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
#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
#15106 Consider probability quantities as real-valued expressions enhancement 2 EasyCrypt pre-1.x

Resolution: None (32 matches)

Ticket Summary Owner Type Priority Component Version
#15891 Instantiating axioms and sub-theories when cloning theories Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#15502 "Ident <top>_[...] is not yet declared" when cloning a theory with operators Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15716 Problem with introduction of Module in Proof Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15762 Tactic to transform a tuple equality into a conjonction Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15779 Inference during apply Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15808 Declaring/defining mixfix operators, using them when not in scope Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15809 Parsing/Printing scope for operator overloading "(x op y)%Scope" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15849 Ignoring proof that are already done in a file Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15854 Allow sequences of variable declarations in procedure definitions Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15859 Omit path when it can be inferred from context Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15879 While one sided ckunz enhancement 3 EasyCrypt pre-1.x
#15880 Constant propagation with module variable Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15907 clone import and clone export Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15917 Proving "a = b => f a = f b" should not require a call to SMT Pierre-Yves Strub enhancement 3 EasyCrypt 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 EasyCrypt pre-1.x
#15921 A strongest post-condition tactic [sp n m], like in trunk ckunz enhancement 3 EasyCrypt pre-1.x
#15968 assertion failure when fun tactic for abstract function isn't given argument Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16082 move * for adversary function outside { ... } Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16292 Side-conditions for the rnd rule in pHL should be proved under some precondition ckunz defect 3 EasyCrypt pre-1.x
#16456 allow expression, formula in cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16560 Non-relational 'bypr' for probabilistic Hoare statements ckunz enhancement 3 EasyCrypt pre-1.x
#16657 Pattern-matching on records Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16723 Subtyping for abstract modules and functors Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#16749 link between hoare bdhoare equiv Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#16763 Simplification should discriminate datatype constructors Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16789 Pattern matching should to some top-level delta-unfolding Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16918 selection tactical "all n" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15817 Lighten EC syntax by removing the clumsy "<:" && "&" notations for modules / memories introductions / applications Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15906 (local) opening of modules Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15912 Be able to inline only one side after an equiv Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15930 Clear all Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#16087 New view for apply: !a -> (a => false) Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x

Resolution: accepted (1 match)

Ticket Summary Owner Type Priority Component Version
#15922 if tactic for bd_hoare doesn't work with precondition true Santiago Zanella-Béguelin defect 3 EasyCrypt pre-1.x
(more results for this group on next page)
1 2 3 4 5
Note: See TracQuery for help on using queries.