Custom query (429 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (301 - 400 of 429)

1 2 3 4 5

Resolution: fixed (42 matches)

Ticket Summary Owner Type Priority Component Version
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 EasyCrypt pre-1.x
#16729 Tactic swap causes inconsistent dependencies Benjamin Grégoire defect 3 EasyCrypt 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
#15974 The following example generates an anomaly Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16691 the name <top> should be accessible to the user. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17276 the pretty printer is getting the relative precedences of unary - and %% wrong Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17252 The `seq` variant documented as pHL is in fact the HL tactic. Alley Stoughton defect 3 Documentation pre-1.x
#15853 timeout and prover settings are not undone Pierre-Yves Strub defect 3 ProofGeneral pre-1.x
#17310 Top-level command to print various databases (exact, rewrite, ...) Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#15990 trivial cannot prove chained relations directly Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#16468 try fails to catch some call-related exceptions defect 3 EasyCrypt pre-1.x
#16457 try tactic not catching case failure Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#15882 tuple and memory misprinted Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17224 type declarations with bad type variables yield anomalies rather than error messages Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15737 Type-soundness issue when implementing module signatures Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15738 Typing functor applications inside modules Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16288 uncatched exception with functor inside functor Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17096 Unfolding should work even in the presence of several matching operators. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17230 unhelpful error message when there are two matching operators with needed type Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17106 Unification should work modulo delta-unfolding / simplification. enhancement 3 EasyCrypt pre-1.x
#15908 Unification variables appear Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16137 universal elimination doesn't enforce { ... } restriction on module Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17112 `unknown symbol Top.o` when importing a theory including objects referring to `Top.o` Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17168 Unsoundness: combination of sections, modules, and choice-operators Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17132 Unsoundness in definition of "glob M" Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17114 Unsoundness of module system Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17027 [Unsoundness] The HL and pHL tactics for abstract function calls do not quantify over variables that may be modified in the postcondition Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17223 use of ' and ` in operator names causes anomaly rather than error message Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17136 variant of seq to deal with large preconditions enhancement 3 EasyCrypt pre-1.x
#17327 Variants of `<*>` with preference Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17196 Vernacular command for dumping env. as a Why3 task. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17177 View application fails non gracely when it cannot instanciate all type variables. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16964 Warn when a variable is used before being initialized Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16772 Weird error with inductives when aliasing constructors Pierre-Yves Strub defect 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
#17061 when arguments to seq are too big, anomaly rather than error message defect 3 EasyCrypt pre-1.x
#16986 "while >=" generates invalid goals ckunz defect 3 EasyCrypt pre-1.x
#17362 wildcard syntax for SMT provers in prover [...] enhancement 3 EasyCrypt pre-1.x
#15910 Wrong precedence for negation "!" Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17214 Wrong printed for memory Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17201 `x-y` and `x + -y` should be convertible Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15676 Zeta tactics takes too much time to end(infinite loop ?) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x

Resolution: invalid (17 matches)

Ticket Summary Owner Type Priority Component Version
#17191 Assert failure Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16512 Bug in pose Pierre-Yves Strub defect 3 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
#15915 conjunctive introduction pattern does not split <=> 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
#17236 error with rewriting occurrence of -1 when only one matching occurrence defect 3 EasyCrypt pre-1.x
#17155 Fix stdlib w.r.t. why3 import Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17401 Generalizations may perform freeness checks in the wrong context 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
#17289 Missing dependencies in OPAM package defect 3 EasyCrypt pre-1.x
#16253 Non-local modules and abstract restrictions. defect 3 EasyCrypt pre-1.x
#17381 Possible bug: no matching operator even when available defect 2 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
#15999 Pretty printer add too much scoping annotations. Pierre-Yves Strub defect 2 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
#17272 Wrong name defect 3 EasyCrypt pre-1.x

Resolution: wontfix (12 matches)

Ticket Summary Owner Type Priority Component Version
#17269 Add notations for >/>= Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17115 [exfalso] tactic for ambient logic enhancement 3 EasyCrypt pre-1.x
#17104 Make (<>) accessible in prefix form enhancement 1 EasyCrypt pre-1.x
#17121 Make Option.witness accessible at top level enhancement 3 EasyCrypt pre-1.x
#17397 odd scoping when overwriting operator in theory cloning enhancement 3 EasyCrypt pre-1.x
#17046 possible tactic renaming: [proc *] -> [eager proc *] Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#15884 Repeat tactic broken 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
#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
#17232 weirdness involving redefining (=) or defining (<>) enhancement 3 EasyCrypt pre-1.x
#17350 witness not in apRHL defect 3 EasyCrypt pre-1.x

Resolution: duplicate (15 matches)

Ticket Summary Owner Type Priority Component Version
#17118 Add the ability to print the axioms of the environment enhancement 3 EasyCrypt pre-1.x
#17154 anomaly: EcPV.MemoryClash defect 3 EasyCrypt pre-1.x
#17146 Bad error message in combination choice/modules/section Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17332 Better localisation when a pattern cannot be infered Pierre-Yves Strub 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
#16628 making nested sections work enhancement 3 EasyCrypt pre-1.x
#15520 request for more loop manipulation tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17108 require clone 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
#17296 Some program tactics (`rnd`) generate invalid formulas when Distr is not loaded defect 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
#16058 Syntax f.x in equiv precondition for fonction argument enhancement 3 EasyCrypt pre-1.x
#17299 Transitivity using an equiv enhancement 3 EasyCrypt phl

Resolution: worksforme (5 matches)

Ticket Summary Owner Type Priority Component Version
#17173 alternative to "require A; clone export A as B" that does not add A to SMT context enhancement 3 EasyCrypt pre-1.x
#17095 anomaly raised by invariant form of [call upto] defect 3 EasyCrypt pre-1.x
#15106 Consider probability quantities as real-valued expressions enhancement 2 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
#17052 Parse error on (**) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x

Resolution: None (9 matches)

Ticket Summary Owner Type Priority Component Version
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#16456 allow expression, formula in cloning 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
#15968 assertion failure when fun tactic for abstract function isn't given argument Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15921 A strongest post-condition tactic [sp n m], like in trunk ckunz enhancement 3 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
#15907 clone import and clone export Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15880 Constant propagation with module variable Pierre-Yves Strub enhancement 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.