#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

#17052 
Parse error on (**)

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

#15809 
Parsing/Printing scope for operator overloading "(x op y)%Scope"

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16657 
Patternmatching on records

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16789 
Pattern matching should to some toplevel deltaunfolding

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17199 
PG: Default weakcheck mode indicator is invalid.

PierreYves Strub

defect

2

ProofGeneral

pre1.x

#15970 
PG does not handle local lemmas properly.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17068 
Possible bug in the unionfind algorithm

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17381 
Possible bug: no matching operator even when available


defect

2

EasyCrypt

pre1.x

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

Benjamin Grégoire

enhancement

3

EasyCrypt

pre1.x

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


defect

3

EasyCrypt

pre1.x

#17260 
pragma +option should fail gracefully.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15999 
Pretty printer add too much scoping annotations.

PierreYves Strub

defect

2

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

#15716 
Problem with introduction of Module in Proof

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

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

PierreYves Strub

enhancement

3

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

#15884 
Repeat tactic broken

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15520 
request for more loop manipulation tactics

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#17108 
require clone


enhancement

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

#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

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


enhancement

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

#16918 
selection tactical "all n"

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

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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

ckunz

defect

3

EasyCrypt

pre1.x

#16763 
Simplification should discriminate datatype constructors

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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


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

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


defect

3

EasyCrypt

pre1.x

#16723 
Subtyping for abstract modules and functors

Benjamin Grégoire

enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16885 
Support for type annotations in let expressions

PierreYves Strub

enhancement

1

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

(more results for this group on next page)
