Custom query (519 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (301 - 400 of 519)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Version Severity
#17338 misspelled pragmas are not reported Pierre-Yves Strub enhancement 3 pre-1.x normal
#17350 witness not in apRHL defect 3 pre-1.x normal
#17352 Question about run easycrypt task 3 pre-1.x normal
#17354 In cloning, `rename` should not be allowed to create unreachable/unparsable symbols Pierre-Yves Strub defect 3 pre-1.x normal
#17355 Pretty-printer sometimes forget to use the abbreviation Pierre-Yves Strub defect 3 pre-1.x normal
#17359 `rewrite ?lem` should fail (hard) if `lem` does not exist in scope enhancement 3 pre-1.x normal
#17361 scoping problem with theory renaming Pierre-Yves Strub defect 3 pre-1.x normal
#17362 wildcard syntax for SMT provers in prover [...] enhancement 3 pre-1.x normal
#17369 imprecise pretty printing with functor application defect 2 pre-1.x normal
#17371 new option for smt Pierre-Yves Strub enhancement 3 pre-1.x normal
#17372 "" and "!" semantic for smt Pierre-Yves Strub enhancement 3 pre-1.x normal
#17373 introduction pattern bug somehow related to SmtMap defect 3 pre-1.x normal
#17375 `include` command for modules / module types Pierre-Yves Strub enhancement 3 pre-1.x normal
#17376 behaviour of module type include in functor types Benjamin Grégoire enhancement 3 pre-1.x normal
#17377 characterization lemmas for <=> and \proper Pierre-Yves Strub enhancement 3 pre-1.x normal
#17381 Possible bug: no matching operator even when available defect 2 pre-1.x normal
#17385 problem sending goal to SMT (involving inductive datatype and higher order function) Pierre-Yves Strub defect 3 pre-1.x normal
#17387 no error message for match Pierre-Yves Strub defect 3 pre-1.x normal
#17389 inline does not inline under match statement defect 3 pre-1.x normal
#17393 Cloning polymorphic datatypes does not allow case analysis defect 3 pre-1.x normal
#17394 anomaly on some smt calls Pierre-Yves Strub defect 3 pre-1.x normal
#15815 Search path for theories should include path of currently active file Pierre-Yves Strub defect 2 pre-1.x minor
#15841 No explicit binding in equiv creates problems Benjamin Grégoire defect 3 pre-1.x minor
#15851 [rnd] for map update produces confusing post-conditions Pierre-Yves Strub defect 3 pre-1.x minor
#15873 Bug Printer Pierre-Yves Strub defect 2 pre-1.x minor
#15882 tuple and memory misprinted Pierre-Yves Strub defect 3 pre-1.x minor
#15892 It should not be possible to close a theory where not all proofs are finished Pierre-Yves Strub defect 3 pre-1.x minor
#15909 first|last tactical do not have the right precedence w.r.t tactics chaining (t1; t2) Pierre-Yves Strub defect 3 pre-1.x minor
#15910 Wrong precedence for negation "!" Pierre-Yves Strub defect 2 pre-1.x minor
#15915 conjunctive introduction pattern does not split <=> Pierre-Yves Strub defect 2 pre-1.x minor
#15949 Improve kill error message Pierre-Yves Strub enhancement 2 pre-1.x minor
#15970 PG does not handle local lemmas properly. Pierre-Yves Strub defect 3 pre-1.x minor
#15990 trivial cannot prove chained relations directly Pierre-Yves Strub defect 2 pre-1.x minor
#16002 bad error message when predicate is given polymorphic constant Pierre-Yves Strub defect 2 pre-1.x minor
#16015 lack of dot in map subscripting leads to assertion failure Pierre-Yves Strub defect 3 pre-1.x minor
#16066 bad line number in error message when run in batch mode Pierre-Yves Strub defect 2 pre-1.x minor
#16067 bad error message when value is treated as function Pierre-Yves Strub defect 2 pre-1.x minor
#16086 Missing error message: "Abstract function <function name> cannot be inlined." Pierre-Yves Strub defect 2 pre-1.x minor
#16102 bad error message when value of constant refers to module variable Pierre-Yves Strub defect 2 pre-1.x minor
#16111 Strange bug in require Pierre-Yves Strub defect 3 pre-1.x minor
#16114 Bad error message Pierre-Yves Strub defect 2 pre-1.x minor
#16150 Multiple import Pierre-Yves Strub defect 2 pre-1.x minor
#16165 "fixed" a breaking test case that may have been left as a TODO Pierre-Yves Strub defect 2 pre-1.x minor
#16226 Some usages of the 'by' tactical do not discharge final trivial goals Pierre-Yves Strub defect 2 pre-1.x minor
#16288 uncatched exception with functor inside functor Pierre-Yves Strub defect 3 pre-1.x minor
#16459 elim failing on pattern-matching let expressions Pierre-Yves Strub defect 2 pre-1.x minor
#16460 elim fails on let statements that can be simplified away Pierre-Yves Strub defect 2 pre-1.x minor
#16512 Bug in pose Pierre-Yves Strub defect 3 pre-1.x minor
#16620 Failure to pattern-match functional terms when they are applied in the goal. Pierre-Yves Strub defect 3 pre-1.x minor
#16656 bug in parser with rewrite? Pierre-Yves Strub defect 3 pre-1.x minor
#16691 the name <top> should be accessible to the user. Pierre-Yves Strub defect 3 pre-1.x minor
#16727 bd_hoare should work on >=, rather than forcing us to swap arguments Benjamin Grégoire defect 3 pre-1.x minor
#16773 "do! rewrite /op" loops Pierre-Yves Strub defect 2 pre-1.x minor
#16840 @ can be used to define infix operators, but cannot be used to apply them Pierre-Yves Strub defect 3 pre-1.x minor
#17018 splitwhile syntax is still weird Pierre-Yves Strub defect 3 pre-1.x minor
#17047 pretty printing of module type uses old notation for "*" defect 3 pre-1.x minor
#17051 Pretty-printing regression defect 3 pre-1.x minor
#17061 when arguments to seq are too big, anomaly rather than error message defect 3 pre-1.x minor
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 pre-1.x minor
#17091 [rewrite] should head-reduce created b-redexes Pierre-Yves Strub enhancement 3 pre-1.x minor
#17092 Chaining [apply] Pierre-Yves Strub enhancement 3 pre-1.x minor
#17093 Add the possibility to declare several operators/predicates in 1 command. Pierre-Yves Strub enhancement 2 pre-1.x minor
#17116 Bad error message for [swap] Pierre-Yves Strub defect 3 pre-1.x minor
#17135 anomaly when intro pattern has wrong form Pierre-Yves Strub defect 3 pre-1.x minor
#17138 "easycrypt -check-all" does not load "Logic" Pierre-Yves Strub defect 3 pre-1.x minor
#17139 Multiple require at once. Pierre-Yves Strub enhancement 3 pre-1.x minor
#17177 View application fails non gracely when it cannot instanciate all type variables. Pierre-Yves Strub defect 3 pre-1.x minor
#17200 Parse error in required theories are incorrectly located. Pierre-Yves Strub defect 3 pre-1.x minor
#17227 Procedures with unit return type should be allowed to return `tt' Pierre-Yves Strub enhancement 2 pre-1.x minor
#17273 `alias` failures look like uncaught exceptions defect 3 pre-1.x minor
#17294 `Self` (and `Top`) should be allowed in module restrictions Pierre-Yves Strub defect 1 pre-1.x minor
#15612 require Theory issues misleading "added" messages Pierre-Yves Strub defect 1 pre-1.x trivial
#15916 Extraneous internal memory identifier "hr" in output Pierre-Yves Strub defect 2 pre-1.x trivial
#15999 Pretty printer add too much scoping annotations. Pierre-Yves Strub defect 2 pre-1.x trivial
#16117 Fail to pose an arbitrary lambda Pierre-Yves Strub defect 2 pre-1.x trivial
#16504 Parse error on complex arguments to functions in probability statements Pierre-Yves Strub defect 2 pre-1.x trivial
#17007 Inconsistent syntax for closing sections/theories enhancement 2 pre-1.x trivial
#17033 Some program logic tactics that modify the precondition use bad associativity Pierre-Yves Strub enhancement 3 pre-1.x trivial
#17060 pretty printer still using "lambda" instead of "fun" defect 3 pre-1.x trivial
#17071 Error message for [expect] <default> enhancement 1 pre-1.x trivial
#17104 Make (<>) accessible in prefix form enhancement 1 pre-1.x trivial
#17115 [exfalso] tactic for ambient logic enhancement 3 pre-1.x trivial
#17121 Make Option.witness accessible at top level enhancement 3 pre-1.x trivial
#17185 Anomalies should give rise to a "This is a bug, please report."-type message. Pierre-Yves Strub enhancement 1 pre-1.x trivial
#17272 Wrong name defect 3 pre-1.x trivial
#17321 `case @[ambient]` needs its syntax unified with that of ambient `case` Pierre-Yves Strub enhancement 3 pre-1.x trivial
#15762 Tactic to transform a tuple equality into a conjonction Pierre-Yves Strub enhancement 3 pre-1.x
#15779 Inference during apply Pierre-Yves Strub enhancement 3 pre-1.x
#15786 Swap with call to the adversary defect 3 pre-1.x
#15808 Declaring/defining mixfix operators, using them when not in scope Pierre-Yves Strub enhancement 3 pre-1.x
#15809 Parsing/Printing scope for operator overloading "(x op y)%Scope" Pierre-Yves Strub enhancement 3 pre-1.x
#15817 Lighten EC syntax by removing the clumsy "<:" && "&" notations for modules / memories introductions / applications Pierre-Yves Strub enhancement 2 pre-1.x
#15827 memory restriction for adversary does not take inner modules into account Benjamin Grégoire defect 3 pre-1.x
#15842 Bug in lambda translation Benjamin Grégoire defect 3 pre-1.x
#15849 Ignoring proof that are already done in a file Pierre-Yves Strub enhancement 3 pre-1.x
#15854 Allow sequences of variable declarations in procedure definitions Pierre-Yves Strub enhancement 3 pre-1.x
#15859 Omit path when it can be inferred from context Pierre-Yves Strub enhancement 3 pre-1.x
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 pre-1.x
#15879 While one sided ckunz enhancement 3 pre-1.x
#15880 Constant propagation with module variable Pierre-Yves Strub enhancement 3 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.