Custom query (528 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (101 - 200 of 528)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Version Severity
#15716 Problem with introduction of Module in Proof Pierre-Yves Strub defect 3 pre-1.x major
#15737 Type-soundness issue when implementing module signatures Pierre-Yves Strub defect 3 pre-1.x major
#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
#15744 require import causes name collisions in sub theories Pierre-Yves Strub defect 3 pre-1.x major
#15762 Tactic to transform a tuple equality into a conjonction Pierre-Yves Strub enhancement 3 pre-1.x
#15764 Result not introduce after call in hoare logic Pierre-Yves Strub defect 3 pre-1.x major
#15768 Inlining with functor and cloning doesn't work Pierre-Yves Strub defect 3 pre-1.x major
#15779 Inference during apply Pierre-Yves Strub enhancement 3 pre-1.x
#15781 Bug into env insertion of a specific axiom Pr[] Pierre-Yves Strub defect 3 pre-1.x major
#15791 import doesn't import function from module Pierre-Yves Strub defect 3 pre-1.x critical
#15794 Operator not found Pierre-Yves Strub defect 3 pre-1.x major
#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
#15813 call tactic signals an "unknown symbol" error Pierre-Yves Strub defect 3 pre-1.x major
#15814 call tactic accepts variable defined in left game ({1}) defined for right game Pierre-Yves Strub defect 3 pre-1.x major
#15815 Search path for theories should include path of currently active file Pierre-Yves Strub defect 2 pre-1.x minor
#15817 Lighten EC syntax by removing the clumsy "<:" && "&" notations for modules / memories introductions / applications Pierre-Yves Strub enhancement 2 pre-1.x
#15849 Ignoring proof that are already done in a file Pierre-Yves Strub enhancement 3 pre-1.x
#15851 [rnd] for map update produces confusing post-conditions Pierre-Yves Strub defect 3 pre-1.x minor
#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
#15871 Stack Overflow Pierre-Yves Strub defect 3 pre-1.x major
#15873 Bug Printer Pierre-Yves Strub defect 2 pre-1.x minor
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 pre-1.x
#15877 Apply is not working when trying to use it to instantiate a lemma that is quantified on modules Pierre-Yves Strub defect 3 pre-1.x blocker
#15880 Constant propagation with module variable Pierre-Yves Strub enhancement 3 pre-1.x
#15881 Complete path for local variable in printer Pierre-Yves Strub defect 3 pre-1.x
#15882 tuple and memory misprinted Pierre-Yves Strub defect 3 pre-1.x minor
#15884 Repeat tactic broken Pierre-Yves Strub defect 3 pre-1.x major
#15891 Instantiating axioms and sub-theories when cloning theories Pierre-Yves Strub enhancement 4 pre-1.x
#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
#15906 (local) opening of modules Pierre-Yves Strub enhancement 2 pre-1.x
#15907 clone import and clone export Pierre-Yves Strub enhancement 3 pre-1.x
#15908 Unification variables appear Pierre-Yves Strub defect 3 pre-1.x normal
#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
#15912 Be able to inline only one side after an equiv Pierre-Yves Strub enhancement 2 pre-1.x
#15915 conjunctive introduction pattern does not split <=> Pierre-Yves Strub defect 2 pre-1.x minor
#15916 Extraneous internal memory identifier "hr" in output Pierre-Yves Strub defect 2 pre-1.x trivial
#15917 Proving "a = b => f a = f b" should not require a call to SMT Pierre-Yves Strub enhancement 3 pre-1.x
#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
#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
#15970 PG does not handle local lemmas properly. Pierre-Yves Strub defect 3 pre-1.x minor
#15975 Cfold bug with notation x.[a] = Pierre-Yves Strub defect 3 pre-1.x major
#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
#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
#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
#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
#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
#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
#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
#16399 Bug in congr? Pierre-Yves Strub defect 3 pre-1.x major
#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
#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
#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
#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
#16746 Losslessness annotations Pierre-Yves Strub enhancement 2 pre-1.x
#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
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.