Custom query (505 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (201 - 300 of 505)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Version Severity
#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
#17033 Some program logic tactics that modify the precondition use bad associativity Pierre-Yves Strub enhancement 3 pre-1.x trivial
#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
#17046 possible tactic renaming: [proc *] -> [eager proc *] Benjamin Grégoire enhancement 3 pre-1.x normal
#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
#17057 Add the possibility to rule out the prover filtering mecanism from the command line. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17059 Negative line selectors in program logic tactics Pierre-Yves Strub enhancement 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
#17066 Better error message when operator selection failed. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17067 Syntax for chained case analysis of the top-assumption Pierre-Yves Strub enhancement 3 pre-1.x normal
#17069 Improve error messages of the (P?R)HL tactics Pierre-Yves Strub enhancement 3 pre-1.x normal
#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
#17075 [sp] should fail when given code positions that cannot be reached Pierre-Yves Strub enhancement 3 pre-1.x normal
#17083 Missing eta-reduction in conversion Benjamin Grégoire enhancement 3 pre-1.x normal
#17084 syntax for non-flat proof-terms Pierre-Yves Strub enhancement 3 pre-1.x normal
#17091 [rewrite] should head-reduce created b-redexes Pierre-Yves Strub enhancement 3 pre-1.x minor
#17092 Chaining [apply] Pierre-Yves Strub enhancement 3 pre-1.x minor
#17095 anomaly raised by invariant form of [call upto] defect 3 pre-1.x normal
#17096 Unfolding should work even in the presence of several matching operators. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17097 Bad pretty-printing of lists. Pierre-Yves Strub defect 3 pre-1.x normal
#17099 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 3 pre-1.x normal
#17100 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 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
#17106 Unification should work modulo delta-unfolding / simplification. enhancement 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
#17108 require clone enhancement 3 pre-1.x normal
#17115 [exfalso] tactic for ambient logic enhancement 3 pre-1.x trivial
#17116 Bad error message for [swap] Pierre-Yves Strub defect 3 pre-1.x minor
#17118 Add the ability to print the axioms of the environment enhancement 3 pre-1.x normal
#17119 Give the ability to print subgoals Pierre-Yves Strub enhancement 3 pre-1.x normal
#17121 Make Option.witness accessible at top level enhancement 3 pre-1.x trivial
#17122 Clone ignores provided proof Pierre-Yves Strub defect 3 pre-1.x normal
#17123 Bad parsing on call (_: B, I) Pierre-Yves Strub defect 3 pre-1.x normal
#17124 allows to specify timeout only for smt. Pierre-Yves Strub defect 3 pre-1.x normal
#17125 Cannot clear variables referring to memory Pierre-Yves Strub defect 3 pre-1.x normal
#17126 Command and command line option for global timeout multiplier. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17128 assert false in rnd. Benjamin Grégoire defect 3 pre-1.x normal
#17129 bug in alias, the introduced variable has not the good type. Benjamin Grégoire defect 3 pre-1.x normal
#17130 "alias i" works only on random instruction. Benjamin Grégoire enhancement 3 pre-1.x normal
#17133 seq for phoare do not check the type of the arguments. Benjamin Grégoire defect 3 pre-1.x normal
#17134 is_lossless F(M).f generate a parse error. Pierre-Yves Strub defect 3 pre-1.x normal
#17135 anomaly when intro pattern has wrong form Pierre-Yves Strub defect 3 pre-1.x minor
#17137 More tactical about goal selections Pierre-Yves Strub enhancement 3 pre-1.x normal
#17138 "easycrypt -check-all" does not load "Logic" Pierre-Yves Strub defect 3 pre-1.x minor
#17139 Multiple require at once. Pierre-Yves Strub enhancement 3 pre-1.x minor
#17142 Anomaly (related to SMT and memories) Benjamin Grégoire defect 3 pre-1.x normal
#17143 Anomaly (free type variables in conseq) Pierre-Yves Strub defect 3 pre-1.x normal
#17144 Module type checking: Unclear error message and probably bug Pierre-Yves Strub defect 3 pre-1.x normal
#17145 "choice" reorders its arguments Pierre-Yves Strub defect 3 pre-1.x normal
#17146 Bad error message in combination choice/modules/section Pierre-Yves Strub defect 3 pre-1.x normal
#17147 Parse error in (some) expressions involving memories Pierre-Yves Strub defect 3 pre-1.x normal
#17151 Abstract theories Pierre-Yves Strub enhancement 3 pre-1.x normal
#17153 seq does not check type of its arguments Pierre-Yves Strub defect 3 pre-1.x normal
#17154 anomaly: EcPV.MemoryClash defect 3 pre-1.x normal
#17158 "<-" for predicates when cloning Pierre-Yves Strub enhancement 3 pre-1.x normal
#17159 expect should support goal selection Pierre-Yves Strub enhancement 3 pre-1.x normal
#17165 not-to-be-proved lemmas Pierre-Yves Strub enhancement 3 pre-1.x normal
#17166 missing syntax for proving all axioms of a theory, its subtheories, etc., when cloning Pierre-Yves Strub enhancement 3 pre-1.x normal
#17167 Better localization of errors when typing a proof-term Pierre-Yves Strub enhancement 3 pre-1.x normal
#17168 Unsoundness: combination of sections, modules, and choice-operators Pierre-Yves Strub defect 3 pre-1.x critical
#17170 Introduce theory for product distribution Pierre-Yves Strub enhancement 3 pre-1.x normal
#17171 mode similar to nocheck that tries smt calls and just prints the locations for the failing calls Pierre-Yves Strub enhancement 3 pre-1.x normal
#17172 Looping on `rewrite !/op` Pierre-Yves Strub defect 3 pre-1.x normal
#17173 alternative to "require A; clone export A as B" that does not add A to SMT context enhancement 3 pre-1.x normal
#17174 Return of the memory explosion defect 3 pre-1.x normal
#17176 [print] should display types even on fixpoints Pierre-Yves Strub enhancement 3 pre-1.x normal
#17177 View application fails non gracely when it cannot instanciate all type variables. Pierre-Yves Strub defect 3 pre-1.x minor
#17178 Generalizing over an empty list should generate a sane name Pierre-Yves Strub defect 3 pre-1.x normal
#17179 `done` should close goals with a direct contradiction in its env. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17180 anomaly: File "src/ecCoreFol.ml", line 1207, characters 19-25: Assertion failed Pierre-Yves Strub defect 3 pre-1.x normal
#17184 parse error involving parameterized module Pierre-Yves Strub defect 3 pre-1.x normal
#17187 anomaly when invalid memory is referenced -- should be proper error message Pierre-Yves Strub defect 3 pre-1.x normal
#17188 Error with smt : lazy defect 3 pre-1.x normal
#17189 Syntax for referring to *local* variables by their long name Pierre-Yves Strub enhancement 3 pre-1.x normal
#17190 progress and progress => //. should be equivalent... Pierre-Yves Strub defect 3 pre-1.x normal
#17191 Assert failure Pierre-Yves Strub defect 3 pre-1.x normal
#17193 Obscure failure on lazy smt with higher-order stuff and booleans Pierre-Yves Strub defect 3 pre-1.x normal
#17196 Vernacular command for dumping env. as a Why3 task. Pierre-Yves Strub enhancement 3 pre-1.x normal
#17198 Spurious failure of rewrite Pierre-Yves Strub defect 3 pre-1.x normal
#17200 Parse error in required theories are incorrectly located. Pierre-Yves Strub defect 3 pre-1.x minor
#17201 `x-y` and `x + -y` should be convertible Pierre-Yves Strub enhancement 3 pre-1.x normal
#17203 Rewrite strangely failling Pierre-Yves Strub defect 3 pre-1.x normal
#17205 New syntax for assignments should be available in immediate definitions Pierre-Yves Strub defect 3 pre-1.x normal
#17206 Missing parens in the pretty printer Pierre-Yves Strub defect 3 pre-1.x normal
#17208 `rewrite ... in ...` Pierre-Yves Strub defect 3 pre-1.x normal
#17211 split causes anomaly when given equality between constructors Pierre-Yves Strub defect 3 pre-1.x normal
#17212 Circular [require] dependencies should be caught instead of blowing up computers Pierre-Yves Strub defect 3 pre-1.x normal
#17214 Wrong printed for memory Pierre-Yves Strub defect 3 pre-1.x normal
#17219 operators don't print the way they are declared Pierre-Yves Strub defect 3 pre-1.x normal
#17220 Shorthand "by" syntax should be supported for "realize" Pierre-Yves Strub 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.