#17371 
new option for smt

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16786 
Nicer treatment of datatype constructors

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17387 
no error message for match

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15841 
No explicit binding in equiv creates problems

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16965 
Nontermination when expanding a procedure whose body contains a generic projector (.`n)

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16141 
Not catched error in split

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17165 
nottobeproved lemmas

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17290 
`n!>>` should work


enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17306 
Operator folding and unfolding not checking type parameters

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15794 
Operator not found

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17148 
Operators should be subject to section restrictions

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#16963 
op/pred nosmt ...

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17074 
Option to destruct disjunctive hypotheses in [progress]

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

#17200 
Parse error in required theories are incorrectly located.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17147 
Parse error in (some) expressions involving memories

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17184 
parse error involving parameterized module

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16504 
Parse error on complex arguments to functions in probability statements

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17280 
Parseonly abbreviations

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17221 
parsing change allowing lemma ... by tactics

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17199 
PG: Default weakcheck mode indicator is invalid.

PierreYves Strub

defect

2

ProofGeneral

pre1.x

#17068 
Possible bug in the unionfind algorithm

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17260 
pragma +option should fail gracefully.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17229 
pretty printer errors with inductive datatypes

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17011 
Prettyprinter in adding too much scoping annotation

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17355 
Prettyprinter sometimes forget to use the abbreviation

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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


defect

3

EasyCrypt

pre1.x

#17228 
pretty printer uses bad syntax for type constructors

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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


defect

3

EasyCrypt

pre1.x

#17051 
Prettyprinting regression


defect

3

EasyCrypt

pre1.x

#17012 
pr_false is badly implemented (unsoundness)

PierreYves Strub

defect

4

EasyCrypt

pre1.x

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16149 
printer bug: parentheses in types

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17315 
[print] on notations is not very useful


defect

3

EasyCrypt

pre1.x

#17254 
print produces misleading results on partially applied functors


defect

3

EasyCrypt

pre1.x

#17242 
`print` should display `nosmt` info

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17176 
[print] should display types even on fixpoints

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15998 
Problem in cloning

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#17398 
problem with new eco facility

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

2

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15769 
ProofGeneral issue with new EasyCrypt: undo step at EOF give Emacs type error

PierreYves Strub

defect

3

ProofGeneral

pre1.x

#17365 
Proof of false using Ring and Reals.

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17379 
Proving unreasonable/false lemmas through AltErgo


defect

5

EasyCrypt

pre1.x

#17352 
Question about run easycrypt


task

3

EasyCrypt

pre1.x

#17094 
Refactoring: code for operators addition.

PierreYves Strub

enhancement

3

Internals

pre1.x

#17304 
Regression on anonymous procedure arguments support

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15744 
require import causes name collisions in sub theories

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15612 
require Theory issues misleading "added" messages

PierreYves Strub

defect

1

EasyCrypt

pre1.x

#17049 
"restart scripting" not working in ProofGeneral


defect

2

ProofGeneral

pre1.x

#15764 
Result not introduce after call in hoare logic

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17213 
Retracting/Resetting should cause easycrypt to reload the prelude

PierreYves Strub

defect

3

ProofGeneral

pre1.x

#17174 
Return of the memory explosion


defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16116 
rewrite /op failed with lambda

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17091 
[rewrite] should headreduce created bredexes

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17203 
Rewrite strangely failling

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15996 
rewriting when using intro patterns to eliminate existentials

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17120 
[rnd] allows to prove false

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#15851 
[rnd] for map update produces confusing postconditions

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16112 
Rnd on different type possible

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17361 
scoping problem with theory renaming

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17317 
`search` should work somewhat better with abbreviations

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

1

EasyCrypt

pre1.x

#17153 
seq does not check type of its arguments

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17082 
SMT tactic should be interruptable.

PierreYves Strub

enhancement

4

EasyCrypt

pre1.x

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15966 
Something wrong with installation script?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17226 
some weirdness with operators of form :+

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17211 
split causes anomaly when given equality between constructors

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17018 
splitwhile syntax is still weird

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17198 
Spurious failure of rewrite

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15871 
Stack Overflow

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16726 
Stack overflow during unification

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16111 
Strange bug in require

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16140 
Strange error in typing

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15742 
Strange error raised during a call to trivial

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16115 
Subst failed

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15786 
Swap with call to the adversary


defect

3

EasyCrypt

pre1.x

#17067 
Syntax for chained case analysis of the topassumption

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

1

EasyCrypt

pre1.x

#17084 
syntax for nonflat proofterms

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

1

EasyCrypt

pre1.x

(more results for this group on next page)
