#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

#17269 
Add notations for >/>=

PierreYves Strub

enhancement

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

#17290 
`n!>>` should work


enhancement

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

#17308 
`rewrite !(A,B)` loops when `B` is not known about

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

#17348 
Intropattern `>` might transform a provable goal to a nonprovable one


defect

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

#17366 
crush losing some context on intermediate substitutions


defect

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

#17385 
problem sending goal to SMT (involving inductive datatype and higher order function)

PierreYves Strub

defect

3

pre1.x

normal

#17386 
crush reduces goal whose conclusion is `y1 = y2 <=> x1 = x2` to false goal


defect

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

#17391 
case works with tuple corresponding to glob M, but not with glob M

PierreYves Strub

defect

3

pre1.x

normal

#17393 
Cloning polymorphic datatypes does not allow case analysis


defect

3

pre1.x

normal

#17394 
anomaly on some smt calls

PierreYves Strub

defect

3

pre1.x

normal

#17397 
odd scoping when overwriting operator in theory cloning


enhancement

3

pre1.x

normal

#17398 
problem with new eco facility

PierreYves Strub

defect

3

pre1.x

normal

#17400 
eco problem: .ec file that uses unchanged .ec file is rechecked even though nothing changed and eco files stable

PierreYves Strub

defect

3

pre1.x

normal

#17401 
Generalizations may perform freeness checks in the wrong context


defect

3

pre1.x

normal

#17403 
Support for `move/(_ _ x): H=> H`

PierreYves Strub

enhancement

3

pre1.x

normal

#15106 
Consider probability quantities as realvalued expressions


enhancement

2

pre1.x

normal

#15815 
Search path for theories should include path of currently active file

PierreYves Strub

defect

2

pre1.x

minor

#15817 
Lighten EC syntax by removing the clumsy "<:" && "&" notations for modules / memories introductions / applications

PierreYves Strub

enhancement

2

pre1.x


#15873 
Bug Printer

PierreYves Strub

defect

2

pre1.x

minor

#15906 
(local) opening of modules

PierreYves Strub

enhancement

2

pre1.x


#15910 
Wrong precedence for negation "!"

PierreYves Strub

defect

2

pre1.x

minor

(more results for this group on next page)
