Custom query (527 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (101 - 200 of 527)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Version Severity
#15921 A strongest post-condition tactic [sp n m], like in trunk ckunz enhancement 3 pre-1.x
#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
#15930 Clear all Pierre-Yves Strub enhancement 2 pre-1.x
#15949 Improve kill error message Pierre-Yves Strub enhancement 2 pre-1.x minor
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 pre-1.x major
#15962 Rewrite Fails because it didn't manage to infer type whereas it could Pierre-Yves Strub defect 3 pre-1.x normal
#15965 Assertion failure in EcEnv Pierre-Yves Strub defect 3 pre-1.x major
#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
#15970 PG does not handle local lemmas properly. Pierre-Yves Strub defect 3 pre-1.x minor
#15974 The following example generates an anomaly Benjamin Grégoire defect 3 pre-1.x
#15975 Cfold bug with notation x.[a] = Pierre-Yves Strub defect 3 pre-1.x major
#15980 inconsistency due to choosing from empty distribution Benjamin Grégoire defect 3 pre-1.x critical
#15981 "delta cpEq" causes an untypable goal to be produced Benjamin Grégoire defect 3 pre-1.x
#15982 Printer bug for partially applied infix operators in prefix form Benjamin Grégoire defect 3 pre-1.x
#15990 trivial cannot prove chained relations directly Pierre-Yves Strub defect 2 pre-1.x minor
#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
#15999 Pretty printer add too much scoping annotations. Pierre-Yves Strub defect 2 pre-1.x trivial
#16000 repeated instantiation and losslessness of 3-argument fun don't work well together Benjamin Grégoire defect 3 pre-1.x major
#16001 Instantiating an internal theory when cloning fails Pierre-Yves Strub defect 3 pre-1.x normal
#16002 bad error message when predicate is given polymorphic constant Pierre-Yves Strub defect 2 pre-1.x minor
#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
#16055 confusion of x{1} and x{2} with x in cut Pierre-Yves Strub enhancement 3 pre-1.x normal
#16058 Syntax f.x in equiv precondition for fonction argument enhancement 3 pre-1.x blocker
#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
#16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 pre-1.x normal
#16082 move * for adversary function outside { ... } Pierre-Yves Strub enhancement 3 pre-1.x
#16086 Missing error message: "Abstract function <function name> cannot be inlined." Pierre-Yves Strub defect 2 pre-1.x minor
#16087 New view for apply: !a -> (a => false) Pierre-Yves Strub enhancement 2 pre-1.x
#16102 bad error message when value of constant refers to module variable Pierre-Yves Strub defect 2 pre-1.x minor
#16104 naming issues enhancement 3 pre-1.x blocker
#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
#16416 FEL completeness - initialization Benjamin Grégoire enhancement 3 pre-1.x normal
#16456 allow expression, formula in cloning Pierre-Yves Strub enhancement 3 pre-1.x
#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
#16560 Non-relational 'bypr' for probabilistic Hoare statements ckunz enhancement 3 pre-1.x
#16620 Failure to pattern-match functional terms when they are applied in the goal. Pierre-Yves Strub defect 3 pre-1.x minor
#16622 Functor-level "lambdas" Benjamin Grégoire enhancement 2 pre-1.x
#16628 making nested sections work enhancement 3 pre-1.x normal
#16629 cloning within sections Pierre-Yves Strub enhancement 3 pre-1.x normal
#16656 bug in parser with rewrite? Pierre-Yves Strub defect 3 pre-1.x minor
#16657 Pattern-matching on records Pierre-Yves Strub enhancement 3 pre-1.x
#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
#16723 Subtyping for abstract modules and functors Benjamin Grégoire enhancement 3 pre-1.x
#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
#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
#16737 "declare op" Pierre-Yves Strub enhancement 3 pre-1.x normal
#16746 Losslessness annotations Pierre-Yves Strub enhancement 2 pre-1.x
#16749 link between hoare bdhoare equiv Benjamin Grégoire enhancement 3 pre-1.x
#16751 hoare should work on fun. Benjamin Grégoire defect 3 pre-1.x normal
#16763 Simplification should discriminate datatype constructors Pierre-Yves Strub enhancement 3 pre-1.x
#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
#16780 Change the test script so the test suites can be run in weak check mode Pierre-Yves Strub enhancement 3 pre-1.x
#16786 Nicer treatment of datatype constructors Pierre-Yves Strub enhancement 3 pre-1.x normal
#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
#16789 Pattern matching should to some top-level delta-unfolding Pierre-Yves Strub enhancement 3 pre-1.x
#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
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.