Custom query (528 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (1 - 100 of 528)

1 2 3 4 5 6

Status: accepted (12 matches)

Ticket Summary Owner Type Priority Version Severity
#17378 Proof of false using smt and Eprover. Pierre-Yves Strub defect 5 pre-1.x critical
#17024 Pattern matching should try to infer memory and module parameters Pierre-Yves Strub enhancement 3 pre-1.x normal
#17034 Generalizing loop fusion Pierre-Yves Strub enhancement 3 pre-1.x normal
#17040 Syntactic sugar for nested if-then-else statements. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17042 Pattern matching in non-normal form. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17070 better error message when difference between goal and lemma is tiny Pierre-Yves Strub enhancement 3 pre-1.x normal
#17141 Wrong module type annotations accepted Pierre-Yves Strub defect 4 pre-1.x normal
#17250 off-by-one error in swap Pierre-Yves Strub defect 3 pre-1.x normal
#17392 problems with glob and delta and matching Pierre-Yves Strub defect 3 pre-1.x normal
#16113 <top> in printer Pierre-Yves Strub defect 2 pre-1.x minor
#17195 Swap with 2 args move as far down as possible Pierre-Yves Strub enhancement 3 pre-1.x minor
#17309 `rewrite /F` when F is a fixpoint should simplify selected occurence for head-iota reduction. Pierre-Yves Strub enhancement 3 pre-1.x minor

Status: assigned (27 matches)

Ticket Summary Owner Type Priority Version Severity
#17181 slow rewriting for large expressions Pierre-Yves Strub defect 3 pre-1.x normal
#17194 anomaly: EcHiGoal.LowApply.NoInstance (in byequiv) Benjamin Grégoire defect 3 pre-1.x normal
#17207 Applicative view Pierre-Yves Strub enhancement 3 pre-1.x normal
#17240 Syntactic sugar for proc. that reduces to a call to an external proc. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17253 EasyCrypt should fail gracefully when applying a tactic on a solved goal. Pierre-Yves Strub defect 2 pre-1.x normal
#17255 Missing unification in `clone...with...` Pierre-Yves Strub enhancement 3 pre-1.x normal
#17256 apply/rewrite should work modulo zeta-reduction. Pierre-Yves Strub defect 3 pre-1.x normal
#17261 `rewrite -/(f _)` should not match its own unfoldings. Pierre-Yves Strub defect 3 pre-1.x normal
#17262 Add the possibility to add rewrite hints to rewrite hint databases. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17263 Multiple incompleteness in `apply` Pierre-Yves Strub defect 3 pre-1.x normal
#17264 Add the possibility to clear lemmas when closing a theory. Pierre-Yves Strub defect 2 pre-1.x normal
#17265 `goal` vernacular command Pierre-Yves Strub defect 3 pre-1.x normal
#17268 Add a tactical that fails when no progress is done. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17269 Add notations for >/>= Pierre-Yves Strub enhancement 3 pre-1.x normal
#17270 `done` should close a goal when `false` is a local hyp. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17271 Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn` Pierre-Yves Strub enhancement 3 pre-1.x normal
#17308 `rewrite !(A,B)` loops when `B` is not known about Pierre-Yves Strub defect 3 pre-1.x normal
#17319 Anomaly triggered by `smt` defect 3 pre-1.x normal
#17334 this message need more information: cannot infer all placeholders Pierre-Yves Strub enhancement 3 pre-1.x normal
#17335 the formula contains free type variables Pierre-Yves Strub enhancement 3 pre-1.x normal
#17347 Search with notations is broken. Pierre-Yves Strub defect 2 pre-1.x normal
#17117 Warning when restrictions over an adversary are empty Benjamin Grégoire enhancement 2 pre-1.x minor
#17222 local clones do not disappear from the environment on section end Pierre-Yves Strub enhancement 3 pre-1.x minor
#17310 Top-level command to print various databases (exact, rewrite, ...) Pierre-Yves Strub defect 2 pre-1.x minor
#17364 Internals: use Batteries maps instead of Why3 ones. Pierre-Yves Strub enhancement 1 pre-1.x minor
#17343 (Optional) warning for old syntax Pierre-Yves Strub enhancement 1 pre-1.x trivial
#17345 Bad printing Pierre-Yves Strub defect 1 pre-1.x trivial

Status: closed (61 matches)

Ticket Summary Owner Type Priority Version Severity
#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
#16058 Syntax f.x in equiv precondition for fonction argument enhancement 3 pre-1.x blocker
#16104 naming issues enhancement 3 pre-1.x blocker
#16229 Substitution issue when quantified module variables have the same name as an existing module defect 3 pre-1.x blocker
#16729 Tactic swap causes inconsistent dependencies Benjamin Grégoire defect 3 pre-1.x blocker
#16787 new conseq issues Benjamin Grégoire defect 5 pre-1.x blocker
#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
#17114 Unsoundness of module system Benjamin Grégoire defect 5 pre-1.x blocker
#17132 Unsoundness in definition of "glob M" Pierre-Yves Strub defect 5 pre-1.x blocker
#17274 Collision in names, local variables unreachable Pierre-Yves Strub defect 3 pre-1.x blocker
#15502 "Ident <top>_[...] is not yet declared" when cloning a theory with operators Pierre-Yves Strub defect 3 pre-1.x critical
#15506 Issues when cloning theories Pierre-Yves Strub defect 3 pre-1.x critical
#15702 Error with multiple require if they contain the same game Pierre-Yves Strub defect 4 pre-1.x critical
#15715 Can't access a variable from a functor in probability formula Pierre-Yves Strub defect 3 pre-1.x critical
#15791 import doesn't import function from module Pierre-Yves Strub defect 3 pre-1.x critical
#15872 fun stopped working ckunz defect 5 pre-1.x critical
#15980 inconsistency due to choosing from empty distribution Benjamin Grégoire defect 3 pre-1.x critical
#16965 Non-termination when expanding a procedure whose body contains a generic projector (.`n) Benjamin Grégoire defect 3 pre-1.x critical
#17012 pr_false is badly implemented (unsoundness) Pierre-Yves Strub defect 4 pre-1.x critical
#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
#17068 Possible bug in the union-find algorithm Pierre-Yves Strub defect 5 pre-1.x critical
#17168 Unsoundness: combination of sections, modules, and choice-operators Pierre-Yves Strub defect 3 pre-1.x critical
#17365 Proof of false using Ring and Reals. Pierre-Yves Strub defect 5 pre-1.x critical
#17379 Proving unreasonable/false lemmas through Alt-Ergo defect 5 pre-1.x critical
#17380 Internal "seq" of pHL tactics is unsound Benjamin Grégoire defect 5 pre-1.x critical
#15651 lambda in operator doesn't work Pierre-Yves Strub defect 3 pre-1.x major
#15676 Zeta tactics takes too much time to end(infinite loop ?) Pierre-Yves Strub defect 3 pre-1.x major
#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
#15744 require import causes name collisions in sub theories Pierre-Yves Strub defect 3 pre-1.x major
#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
#15781 Bug into env insertion of a specific axiom Pr[] Pierre-Yves Strub defect 3 pre-1.x major
#15794 Operator not found Pierre-Yves Strub defect 3 pre-1.x major
#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
#15871 Stack Overflow Pierre-Yves Strub defect 3 pre-1.x major
#15884 Repeat tactic broken Pierre-Yves Strub defect 3 pre-1.x major
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 pre-1.x major
#15965 Assertion failure in EcEnv Pierre-Yves Strub defect 3 pre-1.x major
#15975 Cfold bug with notation x.[a] = Pierre-Yves Strub defect 3 pre-1.x major
#16000 repeated instantiation and losslessness of 3-argument fun don't work well together Benjamin Grégoire defect 3 pre-1.x major
#16013 Bug in theory realization Pierre-Yves Strub defect 3 pre-1.x major
#16054 Bug in theory cloning with theory instanciation and export Pierre-Yves Strub defect 3 pre-1.x major
#16112 Rnd on different type possible Pierre-Yves Strub defect 3 pre-1.x major
#16137 universal elimination doesn't enforce { ... } restriction on module Benjamin Grégoire defect 3 pre-1.x major
#16140 Strange error in typing Pierre-Yves Strub defect 3 pre-1.x major
#16222 Functor application circumvents section-locality Pierre-Yves Strub defect 3 pre-1.x major
#16231 General issues with computation of globals for nested modules Benjamin Grégoire defect 3 pre-1.x major
#16306 Bug in cloning ? Benjamin Grégoire defect 5 pre-1.x major
#16399 Bug in congr? Pierre-Yves Strub defect 3 pre-1.x major
#16775 EasyCrypt insists on typing boolean-returning fixpoints as predicates Pierre-Yves Strub defect 3 pre-1.x major
#16790 Bug when cloning and instantiating an abstract type Pierre-Yves Strub defect 3 pre-1.x major
#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
#17013 EasyCrypt toolchain does not compile anymore on OSX Pierre-Yves Strub defect 5 pre-1.x major
#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
#17112 `unknown symbol Top.o` when importing a theory including objects referring to `Top.o` Pierre-Yves Strub defect 5 pre-1.x major
#17127 Bug in typing of instruction x.[y] = e; Pierre-Yves Strub defect 4 pre-1.x major
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.