#17381 
Possible bug: no matching operator even when available


defect

2

pre1.x

normal

#17046 
possible tactic renaming: [proc *] > [eager proc *]

Benjamin Grégoire

enhancement

3

pre1.x

normal

#17107 
Potential mismatch between spec and lemma versions of the "pHL + HL => pHL" variant of [conseq]


defect

3

pre1.x

normal

#17260 
pragma +option should fail gracefully.

PierreYves Strub

defect

3

pre1.x

normal

#15999 
Pretty printer add too much scoping annotations.

PierreYves Strub

defect

2

pre1.x

trivial

#17229 
pretty printer errors with inductive datatypes

PierreYves Strub

defect

3

pre1.x

normal

#17072 
Pretty Printer Glitches for !(_ = _)

PierreYves Strub

defect

3

pre1.x

normal

#17011 
Prettyprinter in adding too much scoping annotation

PierreYves Strub

defect

2

pre1.x

normal

#17355 
Prettyprinter sometimes forget to use the abbreviation

PierreYves Strub

defect

3

pre1.x

normal

#17060 
pretty printer still using "lambda" instead of "fun"


defect

3

pre1.x

trivial

#17228 
pretty printer uses bad syntax for type constructors

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17047 
pretty printing of module type uses old notation for "*"


defect

3

pre1.x

minor

#17051 
Prettyprinting regression


defect

3

pre1.x

minor

#17012 
pr_false is badly implemented (unsoundness)

PierreYves Strub

defect

4

pre1.x

critical

#15982 
Printer bug for partially applied infix operators in prefix form

Benjamin Grégoire

defect

3

pre1.x


#16149 
printer bug: parentheses in types

PierreYves Strub

defect

3

pre1.x

normal

#17315 
[print] on notations is not very useful


defect

3

pre1.x

normal

#17254 
print produces misleading results on partially applied functors


defect

3

pre1.x

normal

#17242 
`print` should display `nosmt` info

PierreYves Strub

enhancement

3

pre1.x

normal

#17176 
[print] should display types even on fixpoints

PierreYves Strub

enhancement

3

pre1.x

normal

#15998 
Problem in cloning

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#16732 
Problem with functor aliases when outermost module is a parameter

Benjamin Grégoire

defect

3

pre1.x


#15716 
Problem with introduction of Module in Proof

PierreYves Strub

defect

3

pre1.x

major

#17227 
Procedures with unit return type should be allowed to return `tt'

PierreYves Strub

enhancement

2

pre1.x

minor

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

PierreYves Strub

defect

3

pre1.x

normal

#17365 
Proof of false using Ring and Reals.

PierreYves Strub

defect

5

pre1.x

critical

#15917 
Proving "a = b => f a = f b" should not require a call to SMT

PierreYves Strub

enhancement

3

pre1.x


#17379 
Proving unreasonable/false lemmas through AltErgo


defect

5

pre1.x

critical

#17352 
Question about run easycrypt


task

3

pre1.x

normal

#17304 
Regression on anonymous procedure arguments support

PierreYves Strub

defect

3

pre1.x

normal

#16000 
repeated instantiation and losslessness of 3argument fun don't work well together

Benjamin Grégoire

defect

3

pre1.x

major

#15884 
Repeat tactic broken

PierreYves Strub

defect

3

pre1.x

major

#15520 
request for more loop manipulation tactics

PierreYves Strub

enhancement

3

pre1.x

normal

#17108 
require clone


enhancement

3

pre1.x

normal

#15744 
require import causes name collisions in sub theories

PierreYves Strub

defect

3

pre1.x

major

#15612 
require Theory issues misleading "added" messages

PierreYves Strub

defect

1

pre1.x

trivial

#15764 
Result not introduce after call in hoare logic

PierreYves Strub

defect

3

pre1.x

major

#17174 
Return of the memory explosion


defect

3

pre1.x

normal

#15962 
Rewrite Fails because it didn't manage to infer type whereas it could

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

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

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

#16116 
rewrite /op failed with lambda

PierreYves Strub

defect

3

pre1.x

normal

#17091 
[rewrite] should headreduce created bredexes

PierreYves Strub

enhancement

3

pre1.x

minor

#17203 
Rewrite strangely failling

PierreYves Strub

defect

3

pre1.x

normal

#15996 
rewriting when using intro patterns to eliminate existentials

PierreYves Strub

defect

2

pre1.x

normal

#17120 
[rnd] allows to prove false

PierreYves Strub

defect

4

pre1.x

normal

#15851 
[rnd] for map update produces confusing postconditions

PierreYves Strub

defect

3

pre1.x

minor

#16112 
Rnd on different type possible

PierreYves Strub

defect

3

pre1.x

major

#17361 
scoping problem with theory renaming

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

2

pre1.x

minor

#16918 
selection tactical "all n"

PierreYves Strub

enhancement

3

pre1.x


#17294 
`Self` (and `Top`) should be allowed in module restrictions

PierreYves Strub

defect

1

pre1.x

minor

#17153 
seq does not check type of its arguments

PierreYves Strub

defect

3

pre1.x

normal

#17133 
seq for phoare do not check the type of the arguments.

Benjamin Grégoire

defect

3

pre1.x

normal

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

PierreYves Strub

enhancement

3

pre1.x

normal

#16292 
Sideconditions for the rnd rule in pHL should be proved under some precondition

ckunz

defect

3

pre1.x


#16763 
Simplification should discriminate datatype constructors

PierreYves Strub

enhancement

3

pre1.x


#17021 
Some judgmentcombining variants of conseq do not apply to procedures

Benjamin Grégoire

defect

3

pre1.x

normal

#17033 
Some program logic tactics that modify the precondition use bad associativity

PierreYves Strub

enhancement

3

pre1.x

trivial

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


defect

3

pre1.x

normal

#15966 
Something wrong with installation script?

PierreYves Strub

defect

3

pre1.x

normal

#16226 
Some usages of the 'by' tactical do not discharge final trivial goals

PierreYves Strub

defect

2

pre1.x

minor

#17226 
some weirdness with operators of form :+

PierreYves Strub

defect

3

pre1.x

normal

#17211 
split causes anomaly when given equality between constructors

PierreYves Strub

defect

3

pre1.x

normal

#17018 
splitwhile syntax is still weird

PierreYves Strub

defect

3

pre1.x

minor

#17075 
[sp] should fail when given code positions that cannot be reached

PierreYves Strub

enhancement

3

pre1.x

normal

#17198 
Spurious failure of rewrite

PierreYves Strub

defect

3

pre1.x

normal

#15871 
Stack Overflow

PierreYves Strub

defect

3

pre1.x

major

#16726 
Stack overflow during unification

PierreYves Strub

defect

3

pre1.x

normal

#16111 
Strange bug in require

PierreYves Strub

defect

3

pre1.x

minor

#16140 
Strange error in typing

PierreYves Strub

defect

3

pre1.x

major

#15742 
Strange error raised during a call to trivial

PierreYves Strub

defect

3

pre1.x

normal

#16115 
Subst failed

PierreYves Strub

defect

3

pre1.x

normal

#16229 
Substitution issue when quantified module variables have the same name as an existing module


defect

3

pre1.x

blocker

#16723 
Subtyping for abstract modules and functors

Benjamin Grégoire

enhancement

3

pre1.x


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

PierreYves Strub

enhancement

3

pre1.x

normal

#16885 
Support for type annotations in let expressions

PierreYves Strub

enhancement

1

pre1.x


#15786 
Swap with call to the adversary


defect

3

pre1.x


#17067 
Syntax for chained case analysis of the topassumption

PierreYves Strub

enhancement

3

pre1.x

normal

#17204 
Syntax for ignoring the return value of a procedure call

PierreYves Strub

enhancement

1

pre1.x

normal

#17084 
syntax for nonflat proofterms

PierreYves Strub

enhancement

3

pre1.x

normal

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

PierreYves Strub

enhancement

3

pre1.x

normal

#16058 
Syntax f.x in equiv precondition for fonction argument


enhancement

3

pre1.x

blocker

#16073 
Syntax to have ={} working for explicitly quantified memory

PierreYves Strub

enhancement

1

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

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

PierreYves Strub

enhancement

3

pre1.x

normal

#15918 
Tactic for proving an equiv/hoare/bd_hoare goal when the precondition is contradictory

Santiago ZanellaBéguelin

enhancement

3

pre1.x


#15950 
tactics for fundamental lemma

Benjamin Grégoire

enhancement

4

pre1.x

major

#16729 
Tactic swap causes inconsistent dependencies

Benjamin Grégoire

defect

3

pre1.x

blocker

#15762 
Tactic to transform a tuple equality into a conjonction

PierreYves Strub

enhancement

3

pre1.x


#15974 
The following example generates an anomaly

Benjamin Grégoire

defect

3

pre1.x


#16691 
the name <top> should be accessible to the user.

PierreYves Strub

defect

3

pre1.x

minor

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

PierreYves Strub

defect

3

pre1.x

normal

#17299 
Transitivity using an equiv


enhancement

3

phl

normal

#15990 
trivial cannot prove chained relations directly

PierreYves Strub

defect

2

pre1.x

minor

#16468 
try fails to catch some callrelated exceptions


defect

3

pre1.x

normal

#16457 
try tactic not catching case failure

PierreYves Strub

defect

2

pre1.x

normal

(more results for this group on next page)
