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
#17166 missing syntax for proving all axioms of a theory, its subtheories, etc., when cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17167 Better localization of errors when typing a proof-term Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17170 Introduce theory for product distribution Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17171 mode similar to nocheck that tries smt calls and just prints the locations for the failing calls Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17176 [print] should display types even on fixpoints Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17179 `done` should close goals with a direct contradiction in its env. Pierre-Yves Strub enhancement 3 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
#17189 Syntax for referring to *local* variables by their long name 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
#17201 `x-y` and `x + -y` should be convertible Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17204 Syntax for ignoring the return value of a procedure call Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17220 Shorthand "by" syntax should be supported for "realize" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17221 parsing change allowing lemma ... by tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17227 Procedures with unit return type should be allowed to return `tt' Pierre-Yves Strub enhancement 2 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
#17231 check for datatype being inhabited isn't complete, but error message suggests it is Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17234 Allow omission of a procedure's return type when it can be inferred Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17242 `print` should display `nosmt` info Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17247 Interactive proof realisation for `instance` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17248 More precise error messages when non-interactive realization fails Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17249 `AlgTactic` && `Ring` should agree on their axioms. Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17258 Intro pattern for hypothesis duplication Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17266 Clear goal window when no more goals Pierre-Yves Strub enhancement 2 ProofGeneral pre-1.x
#17270 `done` should close a goal when `false` is a local hyp. Pierre-Yves Strub enhancement 5 EasyCrypt pre-1.x
#17280 Parse-only abbreviations Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17284 Support for `={<expr>}` in equiv contracts Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17290 `n!->>` should work enhancement 3 EasyCrypt pre-1.x
#17314 Syntax variants of multiple argument module types don't match ones for parameterized modules Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17321 `case @[ambient]` needs its syntax unified with that of ambient `case` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17327 Variants of `<*>` with preference Pierre-Yves Strub enhancement 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
#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
#17362 wildcard syntax for SMT provers in prover [...] enhancement 3 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
#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
#17403 Support for `move/(_ _ x): H=> H` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17352 Question about run easycrypt task 3 EasyCrypt pre-1.x

Resolution: invalid (17 matches)

Ticket Summary Owner Type Priority Component Version
#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
#15999 Pretty printer add too much scoping annotations. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#16253 Non-local modules and abstract restrictions. defect 3 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
#16512 Bug in pose Pierre-Yves Strub defect 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
#17155 Fix stdlib w.r.t. why3 import Pierre-Yves Strub defect 4 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
#17381 Possible bug: no matching operator even when available defect 2 EasyCrypt pre-1.x
#17401 Generalizations may perform freeness checks in the wrong context 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

Resolution: wontfix (12 matches)

Ticket Summary Owner Type Priority Component Version
#15852 Undo immediately after 'save.' does not work Pierre-Yves Strub defect 1 ProofGeneral pre-1.x
#15884 Repeat tactic broken Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17350 witness not in apRHL defect 3 EasyCrypt pre-1.x
#16374 Visual weak-check indicator enhancement 1 ProofGeneral pre-1.x
#17046 possible tactic renaming: [proc *] -> [eager proc *] Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17104 Make (<>) accessible in prefix form enhancement 1 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
#17269 Add notations for >/>= Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17359 `rewrite ?lem` should fail (hard) if `lem` does not exist in scope enhancement 3 EasyCrypt pre-1.x
#17397 odd scoping when overwriting operator in theory cloning enhancement 3 EasyCrypt pre-1.x

Resolution: duplicate (15 matches)

Ticket Summary Owner Type Priority Component Version
#16229 Substitution issue when quantified module variables have the same name as an existing module defect 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
#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
#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
#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
#15106 Consider probability quantities as real-valued expressions enhancement 2 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

Resolution: None (8 matches)

Ticket Summary Owner Type Priority Component Version
#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
#15968 assertion failure when fun tactic for abstract function isn't given argument Benjamin Grégoire defect 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
#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

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.