#15520 
request for more loop manipulation tactics

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15647 
Can't extract easily function from tuple

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15651 
lambda in operator doesn't work

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15676 
Zeta tactics takes too much time to end(infinite loop ?)

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15715 
Can't access a variable from a functor in probability formula

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15716 
Problem with introduction of Module in Proof

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15737 
Typesoundness issue when implementing module signatures

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15738 
Typing functor applications inside modules

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15742 
Strange error raised during a call to trivial

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15744 
require import causes name collisions in sub theories

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15762 
Tactic to transform a tuple equality into a conjonction

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15764 
Result not introduce after call in hoare logic

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15768 
Inlining with functor and cloning doesn't work

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

#15779 
Inference during apply

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15781 
Bug into env insertion of a specific axiom Pr[]

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15786 
Swap with call to the adversary


defect

3

EasyCrypt

pre1.x

#15791 
import doesn't import function from module

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15794 
Operator not found

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15808 
Declaring/defining mixfix operators, using them when not in scope

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

#15813 
call tactic signals an "unknown symbol" error

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15814 
call tactic accepts variable defined in left game ({1}) defined for right game

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15827 
memory restriction for adversary does not take inner modules into account

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15841 
No explicit binding in equiv creates problems

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15842 
Bug in lambda translation

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15849 
Ignoring proof that are already done in a file

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15851 
[rnd] for map update produces confusing postconditions

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15853 
timeout and prover settings are not undone

PierreYves Strub

defect

3

ProofGeneral

pre1.x

#15854 
Allow sequences of variable declarations in procedure definitions

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15859 
Omit path when it can be inferred from context

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15871 
Stack Overflow

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15877 
Apply is not working when trying to use it to instantiate a lemma that is quantified on modules

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15879 
While one sided

ckunz

enhancement

3

EasyCrypt

pre1.x

#15880 
Constant propagation with module variable

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15881 
Complete path for local variable in printer

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15882 
tuple and memory misprinted

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15884 
Repeat tactic broken

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15892 
It should not be possible to close a theory where not all proofs are finished

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15907 
clone import and clone export

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#15908 
Unification variables appear

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15909 
firstlast tactical do not have the right precedence w.r.t tactics chaining (t1; t2)

PierreYves Strub

defect

3

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

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

Santiago ZanellaBéguelin

enhancement

3

EasyCrypt

pre1.x

#15919 
[case] tactic for bd_hoare is useless

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15920 
[conseq (_ : pre => _)] tactic for bd_hoare doesn't work

Santiago ZanellaBéguelin

defect

3

EasyCrypt

pre1.x

#15921 
A strongest postcondition tactic [sp n m], like in trunk

ckunz

enhancement

3

EasyCrypt

pre1.x

#15922 
if tactic for bd_hoare doesn't work with precondition true

Santiago ZanellaBéguelin

defect

3

EasyCrypt

pre1.x

#15924 
Assertion failed in otherwise provable goal

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

#15965 
Assertion failure in EcEnv

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15966 
Something wrong with installation script?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15968 
assertion failure when fun tactic for abstract function isn't given argument

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15970 
PG does not handle local lemmas properly.

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15974 
The following example generates an anomaly

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15975 
Cfold bug with notation x.[a] =

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#15980 
inconsistency due to choosing from empty distribution

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15981 
"delta cpEq" causes an untypable goal to be produced

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

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

Benjamin Grégoire

defect

3

EasyCrypt

pre1.x

#15998 
Problem in cloning

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

#16001 
Instantiating an internal theory when cloning fails

PierreYves Strub

defect

3

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

#16055 
confusion of x{1} and x{2} with x in cut

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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


enhancement

3

EasyCrypt

pre1.x

#16082 
move * for adversary function outside { ... }

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16104 
naming issues


enhancement

3

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

#16115 
Subst failed

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16116 
rewrite /op failed with lambda

PierreYves Strub

defect

3

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

#16174 
Bug in bdhoare call

ckunz

defect

3

EasyCrypt

pre1.x

#16222 
Functor application circumvents sectionlocality

PierreYves Strub

defect

3

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

#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

#16416 
FEL completeness  initialization

Benjamin Grégoire

enhancement

3

EasyCrypt

pre1.x

#16456 
allow expression, formula in cloning

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16468 
try fails to catch some callrelated exceptions


defect

3

EasyCrypt

pre1.x

#16512 
Bug in pose

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16560 
Nonrelational 'bypr' for probabilistic Hoare statements

ckunz

enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16628 
making nested sections work


enhancement

3

EasyCrypt

pre1.x

#16629 
cloning within sections

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

#16656 
bug in parser with rewrite?

PierreYves Strub

defect

3

EasyCrypt

pre1.x

#16657 
Patternmatching on records

PierreYves Strub

enhancement

3

EasyCrypt

pre1.x

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

PierreYves Strub

defect

3

EasyCrypt

pre1.x

(more results for this group on next page)
