#17178 
Generalizing over an empty list should generate a sane name

PierreYves Strub

defect

3

pre1.x

normal

#17179 
`done` should close goals with a direct contradiction in its env.

PierreYves Strub

enhancement

3

pre1.x

normal

#17180 
anomaly: File "src/ecCoreFol.ml", line 1207, characters 1925: Assertion failed

PierreYves Strub

defect

3

pre1.x

normal

#17184 
parse error involving parameterized module

PierreYves Strub

defect

3

pre1.x

normal

#17187 
anomaly when invalid memory is referenced  should be proper error message

PierreYves Strub

defect

3

pre1.x

normal

#17188 
Error with smt : lazy


defect

3

pre1.x

normal

#17189 
Syntax for referring to *local* variables by their long name

PierreYves Strub

enhancement

3

pre1.x

normal

#17190 
progress and progress => //. should be equivalent...

PierreYves Strub

defect

3

pre1.x

normal

#17191 
Assert failure

PierreYves Strub

defect

3

pre1.x

normal

#17193 
Obscure failure on lazy smt with higherorder stuff and booleans

PierreYves Strub

defect

3

pre1.x

normal

#17196 
Vernacular command for dumping env. as a Why3 task.

PierreYves Strub

enhancement

3

pre1.x

normal

#17198 
Spurious failure of rewrite

PierreYves Strub

defect

3

pre1.x

normal

#17200 
Parse error in required theories are incorrectly located.

PierreYves Strub

defect

3

pre1.x

minor

#17201 
`xy` and `x + y` should be convertible

PierreYves Strub

enhancement

3

pre1.x

normal

#17203 
Rewrite strangely failling

PierreYves Strub

defect

3

pre1.x

normal

#17205 
New syntax for assignments should be available in immediate definitions

PierreYves Strub

defect

3

pre1.x

normal

#17206 
Missing parens in the pretty printer

PierreYves Strub

defect

3

pre1.x

normal

#17208 
`rewrite ... in ...`

PierreYves Strub

defect

3

pre1.x

normal

#17211 
split causes anomaly when given equality between constructors

PierreYves Strub

defect

3

pre1.x

normal

#17212 
Circular [require] dependencies should be caught instead of blowing up computers

PierreYves Strub

defect

3

pre1.x

normal

#17214 
Wrong printed for memory

PierreYves Strub

defect

3

pre1.x

normal

#17219 
operators don't print the way they are declared

PierreYves Strub

defect

3

pre1.x

normal

#17220 
Shorthand "by" syntax should be supported for "realize"

PierreYves Strub

enhancement

3

pre1.x

normal

#17221 
parsing change allowing lemma ... by tactics

PierreYves Strub

enhancement

3

pre1.x

normal

#17223 
use of ' and ` in operator names causes anomaly rather than error message

PierreYves Strub

defect

3

pre1.x

normal

#17224 
type declarations with bad type variables yield anomalies rather than error messages

PierreYves Strub

defect

3

pre1.x

normal

#17226 
some weirdness with operators of form :+

PierreYves Strub

defect

3

pre1.x

normal

#17228 
pretty printer uses bad syntax for type constructors

PierreYves Strub

defect

3

pre1.x

normal

#17229 
pretty printer errors with inductive datatypes

PierreYves Strub

defect

3

pre1.x

normal

#17230 
unhelpful error message when there are two matching operators with needed type

PierreYves Strub

enhancement

3

pre1.x

normal

#17231 
check for datatype being inhabited isn't complete, but error message suggests it is

PierreYves Strub

enhancement

3

pre1.x

normal

#17232 
weirdness involving redefining (=) or defining (<>)


enhancement

3

pre1.x

normal

#17233 
pretty printing issues with _?_:_ and modules

PierreYves Strub

defect

3

pre1.x

normal

#17234 
Allow omission of a procedure's return type when it can be inferred

PierreYves Strub

enhancement

3

pre1.x

normal

#17235 
rewrite ... in ... should allow rewriting in uident not just lident

PierreYves Strub

defect

3

pre1.x

normal

#17236 
error with rewriting occurrence of 1 when only one matching occurrence


defect

3

pre1.x

normal

#17237 
failure of rewrite ... in ...

PierreYves Strub

defect

3

pre1.x

normal

#17238 
anomaly with autorevert intro pattern

PierreYves Strub

defect

3

pre1.x

normal

#17241 
`clone import` not working when realizing axioms.

PierreYves Strub

defect

3

pre1.x

normal

#17242 
`print` should display `nosmt` info

PierreYves Strub

enhancement

3

pre1.x

normal

#17243 
Internal error (anomaly) on proof script

PierreYves Strub

defect

3

pre1.x

normal

#17244 
Imprecise "uninitialized local variables" warning

PierreYves Strub

defect

3

pre1.x

normal

#17247 
Interactive proof realisation for `instance`

PierreYves Strub

enhancement

3

pre1.x

normal

#17248 
More precise error messages when noninteractive realization fails

PierreYves Strub

enhancement

3

pre1.x

normal

#17254 
print produces misleading results on partially applied functors


defect

3

pre1.x

normal

#17258 
Intro pattern for hypothesis duplication

PierreYves Strub

enhancement

3

pre1.x

normal

#17260 
pragma +option should fail gracefully.

PierreYves Strub

defect

3

pre1.x

normal

#17272 
Wrong name


defect

3

pre1.x

trivial

#17273 
`alias` failures look like uncaught exceptions


defect

3

pre1.x

minor

#17274 
Collision in names, local variables unreachable

PierreYves Strub

defect

3

pre1.x

blocker

#17275 
[congr] should apply to iff

PierreYves Strub

defect

3

pre1.x

normal

#17276 
the pretty printer is getting the relative precedences of unary  and %% wrong

PierreYves Strub

defect

3

pre1.x

normal

#17277 
Higherorder patternmatching with quantifiers

PierreYves Strub

defect

3

pre1.x

normal

#17278 
[eta] reduction is not full on multiary functions

github <noreply@…>

defect

3

pre1.x

normal

#17280 
Parseonly abbreviations

PierreYves Strub

enhancement

3

pre1.x

normal

#17284 
Support for `={<expr>}` in equiv contracts

PierreYves Strub

enhancement

3

pre1.x

normal

#17289 
Missing dependencies in OPAM package


defect

3

pre1.x

normal

#17291 
`move: x` should keep the body of `x` if any.

PierreYves Strub

defect

3

pre1.x

normal

#17292 
anomaly on application of a `<=>` lemma to a `=` goal


defect

3

pre1.x

normal

#17293 
Looping behaviour in reduction/simplification. Probably related to reals.

PierreYves Strub

defect

3

pre1.x

normal

#17296 
Some program tactics (`rnd`) generate invalid formulas when Distr is not loaded


defect

3

pre1.x

normal

#17299 
Transitivity using an equiv


enhancement

3

phl

normal

#17300 
Module type checks have wrong variance when dealing with some functor configurations

Benjamin Grégoire

defect

3

pre1.x

normal

#17302 
fel can generate subgoal with undefined memory

Benjamin Grégoire

defect

3

pre1.x

normal

#17303 
more fel peculiarities

Benjamin Grégoire

defect

3

pre1.x

normal

#17304 
Regression on anonymous procedure arguments support

PierreYves Strub

defect

3

pre1.x

normal

#17306 
Operator folding and unfolding not checking type parameters

PierreYves Strub

defect

3

pre1.x

normal

#17312 
cloning can create illformed definitions

PierreYves Strub

defect

3

pre1.x

normal

#17313 
module types with multiple occurrences of same procedure should not be accepted

PierreYves Strub

defect

3

pre1.x

normal

#17314 
Syntax variants of multiple argument module types don't match ones for parameterized modules

PierreYves Strub

enhancement

3

pre1.x

normal

#17315 
[print] on notations is not very useful


defect

3

pre1.x

normal

#17318 
clonetime regexp substitution should apply in the specified order

PierreYves Strub

defect

3

pre1.x

normal

#17320 
anomaly when cloning theory with inductive predicate

PierreYves Strub

defect

3

pre1.x

normal

#17321 
`case @[ambient]` needs its syntax unified with that of ambient `case`

PierreYves Strub

enhancement

3

pre1.x

trivial

#17323 
> ip anomaly

PierreYves Strub

defect

3

pre1.x

normal

#17324 
> ip expands predicates in conclusion

PierreYves Strub

defect

3

pre1.x

normal

#17326 
`+` intropattern may reorder assumptions

PierreYves Strub

defect

3

pre1.x

normal

#17327 
Variants of `<*>` with preference

PierreYves Strub

enhancement

3

pre1.x

normal

#17328 
`_` intropattern should only check if the clear is possible once the rest of the intropattern has been processed


enhancement

3

pre1.x

normal

#17330 
anomaly on `apply/contra`

PierreYves Strub

defect

3

pre1.x

normal

#17331 
Tactic arguments for the `exists` tactic should not be commaseparated

PierreYves Strub

enhancement

3

pre1.x

normal

#17332 
Better localisation when a pattern cannot be infered

PierreYves Strub

enhancement

3

pre1.x

normal

#17333 
We need a `pragma` to stop EasyCrypt from reducing `b => false` into `!b`.

PierreYves Strub

enhancement

3

pre1.x

normal

#17336 
`inline` procedure selection by code position

PierreYves Strub

enhancement

3

pre1.x

normal

#17338 
misspelled pragmas are not reported

PierreYves Strub

enhancement

3

pre1.x

normal

#17350 
witness not in apRHL


defect

3

pre1.x

normal

#17352 
Question about run easycrypt


task

3

pre1.x

normal

#17354 
In cloning, `rename` should not be allowed to create unreachable/unparsable symbols

PierreYves Strub

defect

3

pre1.x

normal

#17355 
Prettyprinter sometimes forget to use the abbreviation

PierreYves Strub

defect

3

pre1.x

normal

#17359 
`rewrite ?lem` should fail (hard) if `lem` does not exist in scope


enhancement

3

pre1.x

normal

#17361 
scoping problem with theory renaming

PierreYves Strub

defect

3

pre1.x

normal

#17362 
wildcard syntax for SMT provers in prover [...]


enhancement

3

pre1.x

normal

#17371 
new option for smt

PierreYves Strub

enhancement

3

pre1.x

normal

#17372 
"" and "!" semantic for smt

PierreYves Strub

enhancement

3

pre1.x

normal

#17373 
introduction pattern bug somehow related to SmtMap


defect

3

pre1.x

normal

#17375 
`include` command for modules / module types

PierreYves Strub

enhancement

3

pre1.x

normal

#17376 
behaviour of module type include in functor types

Benjamin Grégoire

enhancement

3

pre1.x

normal

#17377 
characterization lemmas for <=> and \proper

PierreYves Strub

enhancement

3

pre1.x

normal

#17387 
no error message for match

PierreYves Strub

defect

3

pre1.x

normal

#17389 
inline does not inline under match statement


defect

3

pre1.x

normal

(more results for this group on next page)
