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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16001 
Instantiating an internal theory when cloning fails

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16002 
bad error message when predicate is given polymorphic constant

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16013 
Bug in theory realization

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16015 
lack of dot in map subscripting leads to assertion failure

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16054 
Bug in theory cloning with theory instanciation and export

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16066 
bad line number in error message when run in batch mode

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16067 
bad error message when value is treated as function

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16086 
Missing error message: "Abstract function <function name> cannot be inlined."

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16102 
bad error message when value of constant refers to module variable

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16111 
Strange bug in require

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16112 
Rnd on different type possible

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16114 
Bad error message

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16115 
Subst failed

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16116 
rewrite /op failed with lambda

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16117 
Fail to pose an arbitrary lambda

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16137 
universal elimination doesn't enforce { ... } restriction on module

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16138 
assertion failure when call tactic not given { ... } module restriction

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16140 
Strange error in typing

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16141 
Not catched error in split

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16149 
printer bug: parentheses in types

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16150 
Multiple import

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16165 
"fixed" a breaking test case that may have been left as a TODO

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16174 
Bug in bdhoare call

ckunz

defect

3

EasyCrypt

pre1.x

#16222 
Functor application circumvents sectionlocality

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

#16228 
glob M computation problem with functors and inner modules for {*}

Benjamin Grégoire

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

#16231 
General issues with computation of globals for nested modules

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16253 
Nonlocal modules and abstract restrictions.


defect

3

EasyCrypt

pre1.x

#16264 
Bug in rewrite with let

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16288 
uncatched exception with functor inside functor

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

ckunz

defect

3

EasyCrypt

pre1.x

#16306 
Bug in cloning ?

Benjamin Grégoire

defect

5

EasyCrypt

pre1.x

#16362 
Assertion failure when cloning a theory with let expressions

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16399 
Bug in congr?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16457 
try tactic not catching case failure

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16459 
elim failing on patternmatching let expressions

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16460 
elim fails on let statements that can be simplified away

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16468 
try fails to catch some callrelated exceptions


defect

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16512 
Bug in pose

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16620 
Failure to patternmatch functional terms when they are applied in the goal.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16656 
bug in parser with rewrite?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16663 
Goal window should update on tactic failure...

PierreYves Strub

defect

2

ProofGeneral

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16692 
bug in apply.

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#16726 
Stack overflow during unification

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16727 
bd_hoare should work on >=, rather than forcing us to swap arguments

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16729 
Tactic swap causes inconsistent dependencies

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16751 
hoare should work on fun.

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16772 
Weird error with inductives when aliasing constructors

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16773 
"do! rewrite /op" loops

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#16775 
EasyCrypt insists on typing booleanreturning fixpoints as predicates

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16787 
new conseq issues

Benjamin Grégoire

defect

5

EasyCrypt

pre1.x

#16788 
Another stack overflow during unification

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16790 
Bug when cloning and instantiating an abstract type

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16811 
inline * should not try to inline abstract function

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16840 
@ can be used to define infix operators, but cannot be used to apply them

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16849 
Broken proc (in branch 1.0)

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#16856 
Blocker typing bug in rnd (master)

PierreYves Strub

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

#16966 
Many lexer errors related to the universal projector notation (.'n)

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16983 
equiv generates illtyped formulas on illtyped input (instead of an error)

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16984 
Anomaly due to inlining functions with tuple arguments

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16986 
"while >=" generates invalid goals

ckunz

defect

3

EasyCrypt

pre1.x

#16990 
Generalization does not cross tuple projections.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17006 
Instantiating an abstract procedure taking nuple with a nary concrete procedure

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17009 
1.x error messages

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17011 
Prettyprinter in adding too much scoping annotation

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17012 
pr_false is badly implemented (unsoundness)

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17013 
EasyCrypt toolchain does not compile anymore on OSX

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17018 
splitwhile syntax is still weird

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#17026 
EasyCrypt does not compile on Windows (win32 / cygwin)

PierreYves Strub

defect

2

EasyCrypt

pre1.x

#17027 
[Unsoundness] The HL and pHL tactics for abstract function calls do not quantify over variables that may be modified in the postcondition

PierreYves Strub

defect

5

EasyCrypt

pre1.x

#17035 
AltErgo succeeds on false obligations in weird circumstances

PierreYves Strub

defect

4

EasyCrypt

pre1.x

#17038 
Message with anomaly

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17044 
Bad inlining when giving an argument of type unit to a procedure that expects no arguments

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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


defect

3

EasyCrypt

pre1.x

#17049 
"restart scripting" not working in ProofGeneral


defect

2

ProofGeneral

pre1.x

#17050 
elim/let anomaly

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17051 
Prettyprinting regression


defect

3

EasyCrypt

pre1.x

#17052 
Parse error on (**)

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17053 
Bogus goal when variable shadows a module

PierreYves Strub

defect

3

EasyCrypt

pre1.x

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


defect

3

EasyCrypt

pre1.x

#17061 
when arguments to seq are too big, anomaly rather than error message


defect

3

EasyCrypt

pre1.x

#17065 
Invalid priority of `by` w.r.t `;`

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17068 
Possible bug in the unionfind algorithm

PierreYves Strub

defect

5

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17073 
`case` intropattern does not try to headreduce if the goal is not subject to intro.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17078 
EasyCrypt should use big integers internally.

PierreYves Strub

defect

3

Internals

pre1.x

#17079 
Make the testsuite pass.

PierreYves Strub

defect

5

Libraries

pre1.x

#17080 
`t_generalize_hyps` does not work when given a nonsingleton list.

PierreYves Strub

defect

4

Internals

pre1.x

#17089 
anomaly in [sim]

Benjamin Grégoire

defect

4

EasyCrypt

pre1.x

#17095 
anomaly raised by invariant form of [call upto]


defect

3

EasyCrypt

pre1.x

#17097 
Bad prettyprinting of lists.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17101 
[anomaly] when defining an operator over a concrete module's globals

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#17102 
[anomaly] when pHL => pRHL variant of conseq is used with a bound different from [=1%r]

PierreYves Strub

defect

3

EasyCrypt

pre1.x

(more results for this group on next page)
