Custom query (536 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (401 - 500 of 536)

1 2 3 4 5 6

Status: closed (51 matches)

Ticket Summary Owner Type Priority Version Severity
#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
#15873 Bug Printer Pierre-Yves Strub defect 2 pre-1.x minor
#15906 (local) opening of modules Pierre-Yves Strub enhancement 2 pre-1.x
#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
#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
#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
#15999 Pretty printer add too much scoping annotations. Pierre-Yves Strub defect 2 pre-1.x trivial
#16002 bad error message when predicate is given polymorphic constant Pierre-Yves Strub defect 2 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
#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
#16114 Bad error message Pierre-Yves Strub defect 2 pre-1.x minor
#16117 Fail to pose an arbitrary lambda Pierre-Yves Strub defect 2 pre-1.x trivial
#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
#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
#16622 Functor-level "lambdas" Benjamin Grégoire enhancement 2 pre-1.x
#16746 Losslessness annotations Pierre-Yves Strub enhancement 2 pre-1.x
#16773 "do! rewrite /op" loops Pierre-Yves Strub defect 2 pre-1.x minor
#17007 Inconsistent syntax for closing sections/theories enhancement 2 pre-1.x trivial
#17011 Pretty-printer in adding too much scoping annotation Pierre-Yves Strub defect 2 pre-1.x normal
#17026 EasyCrypt does not compile on Windows (win32 / cygwin) Pierre-Yves Strub defect 2 pre-1.x normal
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 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
#17110 [anomaly] on using [call] with a lemma referring to the wrong procedure Pierre-Yves Strub defect 2 pre-1.x normal
#17227 Procedures with unit return type should be allowed to return `tt' Pierre-Yves Strub enhancement 2 pre-1.x minor
#17249 `AlgTactic` && `Ring` should agree on their axioms. Pierre-Yves Strub enhancement 2 pre-1.x normal
#17310 Top-level command to print various databases (exact, rewrite, ...) Pierre-Yves Strub defect 2 pre-1.x minor
#17369 imprecise pretty printing with functor application defect 2 pre-1.x normal
#17381 Possible bug: no matching operator even when available defect 2 pre-1.x normal
#15612 require Theory issues misleading "added" messages Pierre-Yves Strub defect 1 pre-1.x trivial
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 pre-1.x
#16073 Syntax to have ={} working for explicitly quantified memory Pierre-Yves Strub enhancement 1 pre-1.x normal
#16885 Support for type annotations in let expressions Pierre-Yves Strub enhancement 1 pre-1.x
#17071 Error message for [expect] <default> enhancement 1 pre-1.x trivial
#17104 Make (<>) accessible in prefix form enhancement 1 pre-1.x trivial
#17185 Anomalies should give rise to a "This is a bug, please report."-type message. Pierre-Yves Strub enhancement 1 pre-1.x trivial
#17204 Syntax for ignoring the return value of a procedure call Pierre-Yves Strub enhancement 1 pre-1.x normal
#17294 `Self` (and `Top`) should be allowed in module restrictions Pierre-Yves Strub defect 1 pre-1.x minor

Status: new (49 matches)

Ticket Summary Owner Type Priority Version Severity
#17257 `/=` is too weak. defect 5 pre-1.x normal
#17163 Check that `phoare` tactics are forcing the input bounds to be in [0..1]. task 4 pre-1.x major
#17298 Super rnd enhancement 4 phl blocker
#16103 scoping issue with theories enhancement 3 pre-1.x
#16987 Move facts from precondition to context enhancement 3 pre-1.x normal
#17002 Better section && cloning support Pierre-Yves Strub task 3 pre-1.x major
#17022 Pattern-matching on variables in judgments and probability expressions enhancement 3 pre-1.x normal
#17085 Generic Notations Pierre-Yves Strub enhancement 3 pre-1.x normal
#17086 Generalize [rewrite Pr] enhancement 3 pre-1.x normal
#17105 [transitivity] for phoare and hoare enhancement 3 pre-1.x normal
#17113 Decide what to do on rewrite with defined head symbols enhancement 3 pre-1.x normal
#17140 Pattern matching should make use of simplification rules. enhancement 3 pre-1.x normal
#17149 Expand glob A for concrete module enhancement 3 pre-1.x normal
#17156 New vernacular command: `print axiom` enhancement 3 pre-1.x normal
#17164 behavior of -check-all enhancement 3 pre-1.x normal
#17169 Anonymous functor arguments: passing procedures to functors directly enhancement 3 pre-1.x normal
#17175 Direct intro on negative goals enhancement 3 pre-1.x normal
#17192 Problem with `glob` and type inference defect 3 pre-1.x normal
#17197 Asserts in equivalence proofs enhancement 3 pre-1.x normal
#17202 Add seq* tactic enhancement 3 pre-1.x major
#17210 Pattern-matching for pairs in operator arguments enhancement 3 pre-1.x normal
#17215 Issues with module typing when functor parameters are themselves functors defect 3 pre-1.x normal
#17217 need better error message when attempting to apply lemma to goal that isn't a judgment enhancement 3 pre-1.x normal
#17218 proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate enhancement 3 pre-1.x normal
#17225 Explore reproducible smt calls enhancement 3 pre-1.x normal
#17239 Mutual inductive types. enhancement 3 pre-1.x normal
#17245 Formula manipulation commands (for `conseq` and `seq`) enhancement 3 pre-1.x normal
#17246 `rewrite`, apply, ... in contracts defect 3 pre-1.x normal
#17251 print Self enhancement 3 pre-1.x normal
#17267 `auto` with `call` enhancement 3 pre-1.x normal
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` enhancement 3 pre-1.x normal
#17281 Several problems with `apply` in program logics enhancement 3 pre-1.x normal
#17282 call should not work task 3 phl normal
#17283 pattern matching complexity problem defect 3 pre-1.x normal
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. enhancement 3 pre-1.x normal
#17286 pRHL `apply` should have a framing variant enhancement 3 pre-1.x normal
#17287 Program transformation tactics should not `anomaly` without a side in pRHL defect 3 pre-1.x normal
#17288 EasyCrypt crashes when printing required abstract theory IterProc defect 3 pre-1.x normal
#17295 local ops enhancement 3 pre-1.x normal
#17301 Applicative view for `if then else` enhancement 3 pre-1.x normal
#17305 proc* in eager case needlessly assigns result of procedures returning unit to variables enhancement 3 pre-1.x normal
#17311 `smt (@Self)` enhancement 3 pre-1.x normal
#17316 [smt (@Theory)] should force the use of axioms marked as `nosmt` defect 3 pre-1.x normal
#17322 use of side with HL version of while tactic should be syntax error defect 3 pre-1.x normal
#17325 syntax marking end of cloning realization enhancement 3 pre-1.x normal
#17337 substitutions should complain when substituting a locally defined variable enhancement 3 pre-1.x normal
#17340 cfold should support variables (and more general terms). enhancement 3 pre-1.x normal
#17341 for loops enhancement 3 pre-1.x normal
#17342 Better support for rewriting with equivalences enhancement 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.