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
#16013 Bug in theory realization Pierre-Yves Strub defect 3 pre-1.x major
#16015 lack of dot in map subscripting leads to assertion failure Pierre-Yves Strub defect 3 pre-1.x minor
#16054 Bug in theory cloning with theory instanciation and export Pierre-Yves Strub defect 3 pre-1.x major
#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
#16112 Rnd on different type possible Pierre-Yves Strub defect 3 pre-1.x major
#16114 Bad error message Pierre-Yves Strub defect 2 pre-1.x minor
#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
#16117 Fail to pose an arbitrary lambda Pierre-Yves Strub defect 2 pre-1.x trivial
#16137 universal elimination doesn't enforce { ... } restriction on module Benjamin Grégoire defect 3 pre-1.x major
#16138 assertion failure when call tactic not given { ... } module restriction Benjamin Grégoire defect 3 pre-1.x normal
#16140 Strange error in typing Pierre-Yves Strub defect 3 pre-1.x major
#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
#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
#16174 Bug in bdhoare call ckunz defect 3 pre-1.x normal
#16222 Functor application circumvents section-locality Pierre-Yves Strub defect 3 pre-1.x major
#16226 Some usages of the 'by' tactical do not discharge final trivial goals Pierre-Yves Strub defect 2 pre-1.x minor
#16228 glob M computation problem with functors and inner modules for {*} Benjamin Grégoire defect 3 pre-1.x normal
#16229 Substitution issue when quantified module variables have the same name as an existing module defect 3 pre-1.x blocker
#16231 General issues with computation of globals for nested modules Benjamin Grégoire defect 3 pre-1.x major
#16253 Non-local modules and abstract restrictions. defect 3 pre-1.x
#16264 Bug in rewrite with let Pierre-Yves Strub defect 3 pre-1.x normal
#16288 uncatched exception with functor inside functor Pierre-Yves Strub defect 3 pre-1.x minor
#16292 Side-conditions for the rnd rule in pHL should be proved under some precondition ckunz defect 3 pre-1.x
#16306 Bug in cloning ? Benjamin Grégoire defect 5 pre-1.x major
#16362 Assertion failure when cloning a theory with let expressions Benjamin Grégoire defect 3 pre-1.x
#16399 Bug in congr? Pierre-Yves Strub defect 3 pre-1.x major
#16457 try tactic not catching case failure Pierre-Yves Strub defect 2 pre-1.x normal
#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
#16468 try fails to catch some call-related exceptions defect 3 pre-1.x normal
#16504 Parse error on complex arguments to functions in probability statements Pierre-Yves Strub defect 2 pre-1.x trivial
#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
#16692 bug in apply. Pierre-Yves Strub defect 4 pre-1.x normal
#16726 Stack overflow during unification Pierre-Yves Strub defect 3 pre-1.x normal
#16727 bd_hoare should work on >=, rather than forcing us to swap arguments Benjamin Grégoire defect 3 pre-1.x minor
#16729 Tactic swap causes inconsistent dependencies Benjamin Grégoire defect 3 pre-1.x blocker
#16732 Problem with functor aliases when outermost module is a parameter Benjamin Grégoire defect 3 pre-1.x
#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
#16773 "do! rewrite /op" loops Pierre-Yves Strub defect 2 pre-1.x minor
#16775 EasyCrypt insists on typing boolean-returning fixpoints as predicates Pierre-Yves Strub defect 3 pre-1.x major
#16787 new conseq issues Benjamin Grégoire defect 5 pre-1.x blocker
#16788 Another stack overflow during unification Pierre-Yves Strub defect 3 pre-1.x normal
#16790 Bug when cloning and instantiating an abstract type Pierre-Yves Strub defect 3 pre-1.x major
#16811 inline * should not try to inline abstract function Pierre-Yves Strub defect 3 pre-1.x normal
#16840 @ can be used to define infix operators, but cannot be used to apply them Pierre-Yves Strub defect 3 pre-1.x minor
#16849 Broken proc (in branch 1.0) Benjamin Grégoire defect 3 pre-1.x blocker
#16856 Blocker typing bug in rnd (master) Pierre-Yves Strub defect 3 pre-1.x blocker
#16965 Non-termination when expanding a procedure whose body contains a generic projector (.`n) Benjamin Grégoire defect 3 pre-1.x critical
#16966 Many lexer errors related to the universal projector notation (.'n) Pierre-Yves Strub defect 3 pre-1.x normal
#16983 equiv generates ill-typed formulas on ill-typed input (instead of an error) Pierre-Yves Strub defect 3 pre-1.x major
#16984 Anomaly due to inlining functions with tuple arguments Pierre-Yves Strub defect 3 pre-1.x major
#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
#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
#17012 pr_false is badly implemented (unsoundness) Pierre-Yves Strub defect 4 pre-1.x critical
#17013 EasyCrypt toolchain does not compile anymore on OSX Pierre-Yves Strub defect 5 pre-1.x major
#17018 splitwhile syntax is still weird Pierre-Yves Strub defect 3 pre-1.x minor
#17021 Some judgment-combining variants of conseq do not apply to procedures Benjamin Grégoire defect 3 pre-1.x normal
#17026 EasyCrypt does not compile on Windows (win32 / cygwin) Pierre-Yves Strub defect 2 pre-1.x normal
#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 pre-1.x critical
#17035 Alt-Ergo succeeds on false obligations in weird circumstances Pierre-Yves Strub defect 4 pre-1.x critical
#17038 Message with anomaly Pierre-Yves Strub defect 3 pre-1.x normal
#17044 Bad inlining when giving an argument of type unit to a procedure that expects no arguments Pierre-Yves Strub defect 3 pre-1.x major
#17047 pretty printing of module type uses old notation for "*" defect 3 pre-1.x minor
#17050 elim/let anomaly Pierre-Yves Strub defect 3 pre-1.x normal
#17051 Pretty-printing regression defect 3 pre-1.x minor
#17052 Parse error on (**) Pierre-Yves Strub defect 3 pre-1.x normal
#17053 Bogus goal when variable shadows a module Pierre-Yves Strub defect 3 pre-1.x normal
#17060 pretty printer still using "lambda" instead of "fun" defect 3 pre-1.x trivial
#17061 when arguments to seq are too big, anomaly rather than error message defect 3 pre-1.x minor
#17065 Invalid priority of `by` w.r.t `;` Pierre-Yves Strub defect 3 pre-1.x normal
#17068 Possible bug in the union-find algorithm Pierre-Yves Strub defect 5 pre-1.x critical
#17072 Pretty Printer Glitches for !(_ = _) Pierre-Yves Strub defect 3 pre-1.x normal
#17073 `case` intro-pattern does not try to head-reduce if the goal is not subject to intro. Pierre-Yves Strub defect 3 pre-1.x normal
#17089 anomaly in [sim] Benjamin Grégoire defect 4 pre-1.x normal
#17095 anomaly raised by invariant form of [call upto] defect 3 pre-1.x normal
#17097 Bad pretty-printing of lists. Pierre-Yves Strub defect 3 pre-1.x normal
#17101 [anomaly] when defining an operator over a concrete module's globals Pierre-Yves Strub defect 3 pre-1.x normal
#17102 [anomaly] when pHL => pRHL variant of conseq is used with a bound different from [=1%r] Pierre-Yves Strub defect 3 pre-1.x normal
#17107 Potential mismatch between spec and lemma versions of the "pHL + HL => pHL" variant of [conseq] defect 3 pre-1.x normal
#17109 Hoare adversary rule introducess references to non-existent memories in postconditions Benjamin Grégoire defect 5 pre-1.x normal
#17110 [anomaly] on using [call] with a lemma referring to the wrong procedure Pierre-Yves Strub defect 2 pre-1.x normal
#17112 `unknown symbol Top.o` when importing a theory including objects referring to `Top.o` Pierre-Yves Strub defect 5 pre-1.x major
#17114 Unsoundness of module system Benjamin Grégoire defect 5 pre-1.x blocker
#17116 Bad error message for [swap] Pierre-Yves Strub defect 3 pre-1.x minor
#17120 [rnd] allows to prove false Pierre-Yves Strub defect 4 pre-1.x normal
#17122 Clone ignores provided proof Pierre-Yves Strub 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.