Custom query (519 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (101 - 200 of 519)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Version Severity
#17321 `case @[ambient]` needs its syntax unified with that of ambient `case` Pierre-Yves Strub enhancement 3 pre-1.x trivial
#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
#15106 Consider probability quantities as real-valued expressions enhancement 2 pre-1.x normal
#15520 request for more loop manipulation tactics Pierre-Yves Strub enhancement 3 pre-1.x normal
#15647 Can't extract easily function from tuple Pierre-Yves Strub defect 3 pre-1.x normal
#15738 Typing functor applications inside modules Pierre-Yves Strub defect 3 pre-1.x normal
#15742 Strange error raised during a call to trivial Pierre-Yves Strub defect 3 pre-1.x normal
#15908 Unification variables appear Pierre-Yves Strub defect 3 pre-1.x normal
#15922 if tactic for bd_hoare doesn't work with precondition true Santiago Zanella-Béguelin defect 3 pre-1.x normal
#15924 Assertion failed in otherwise provable goal Pierre-Yves Strub defect 3 pre-1.x normal
#15962 Rewrite Fails because it didn't manage to infer type whereas it could Pierre-Yves Strub defect 3 pre-1.x normal
#15966 Something wrong with installation script? Pierre-Yves Strub defect 3 pre-1.x normal
#15968 assertion failure when fun tactic for abstract function isn't given argument Benjamin Grégoire defect 3 pre-1.x normal
#15996 rewriting when using intro patterns to eliminate existentials Pierre-Yves Strub defect 2 pre-1.x normal
#15998 Problem in cloning Pierre-Yves Strub defect 3 pre-1.x normal
#16001 Instantiating an internal theory when cloning fails Pierre-Yves Strub defect 3 pre-1.x normal
#16055 confusion of x{1} and x{2} with x in cut Pierre-Yves Strub enhancement 3 pre-1.x normal
#16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 pre-1.x normal
#16115 Subst failed Pierre-Yves Strub defect 3 pre-1.x normal
#16116 rewrite /op failed with lambda Pierre-Yves Strub defect 3 pre-1.x normal
#16138 assertion failure when call tactic not given { ... } module restriction Benjamin Grégoire defect 3 pre-1.x normal
#16141 Not catched error in split Pierre-Yves Strub defect 3 pre-1.x normal
#16149 printer bug: parentheses in types Pierre-Yves Strub defect 3 pre-1.x normal
#16174 Bug in bdhoare call ckunz defect 3 pre-1.x normal
#16228 glob M computation problem with functors and inner modules for {*} Benjamin Grégoire defect 3 pre-1.x normal
#16264 Bug in rewrite with let Pierre-Yves Strub defect 3 pre-1.x normal
#16416 FEL completeness - initialization Benjamin Grégoire enhancement 3 pre-1.x normal
#16457 try tactic not catching case failure Pierre-Yves Strub defect 2 pre-1.x normal
#16468 try fails to catch some call-related exceptions defect 3 pre-1.x normal
#16628 making nested sections work enhancement 3 pre-1.x normal
#16629 cloning within sections Pierre-Yves Strub enhancement 3 pre-1.x normal
#16692 bug in apply. Pierre-Yves Strub defect 4 pre-1.x normal
#16725 Intro pattern for substitution Pierre-Yves Strub enhancement 3 pre-1.x normal
#16726 Stack overflow during unification Pierre-Yves Strub defect 3 pre-1.x normal
#16737 "declare op" Pierre-Yves Strub enhancement 3 pre-1.x normal
#16751 hoare should work on fun. Benjamin Grégoire defect 3 pre-1.x normal
#16772 Weird error with inductives when aliasing constructors Pierre-Yves Strub defect 3 pre-1.x normal
#16786 Nicer treatment of datatype constructors Pierre-Yves Strub enhancement 3 pre-1.x normal
#16788 Another stack overflow during unification Pierre-Yves Strub defect 3 pre-1.x normal
#16811 inline * should not try to inline abstract function Pierre-Yves Strub defect 3 pre-1.x normal
#16963 op/pred nosmt ... Pierre-Yves Strub enhancement 3 pre-1.x normal
#16964 Warn when a variable is used before being initialized Pierre-Yves Strub enhancement 3 pre-1.x normal
#16966 Many lexer errors related to the universal projector notation (.'n) Pierre-Yves Strub defect 3 pre-1.x normal
#16986 "while >=" generates invalid goals ckunz defect 3 pre-1.x normal
#16990 Generalization does not cross tuple projections. Pierre-Yves Strub defect 3 pre-1.x normal
#17005 Higher-order pattern matching enhancement 3 pre-1.x normal
#17006 Instantiating an abstract procedure taking n-uple with a n-ary concrete procedure Pierre-Yves Strub defect 3 pre-1.x normal
#17009 1.x error messages Pierre-Yves Strub defect 3 pre-1.x normal
#17011 Pretty-printer in adding too much scoping annotation Pierre-Yves Strub defect 2 pre-1.x normal
#17016 Make elim and case work on tuples and records. Retire the special lemmas Pierre-Yves Strub enhancement 3 pre-1.x normal
#17021 Some judgment-combining variants of conseq do not apply to procedures Benjamin Grégoire defect 3 pre-1.x normal
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.