#15968 |
assertion failure when fun tactic for abstract function isn't given argument
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#15974 |
The following example generates an anomaly
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
|
#15980 |
inconsistency due to choosing from empty distribution
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
critical
|
#15981 |
"delta cpEq" causes an untypable goal to be produced
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
|
#15982 |
Printer bug for partially applied infix operators in prefix form
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
|
#16000 |
repeated instantiation and losslessness of 3-argument fun don't work well together
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
major
|
#16137 |
universal elimination doesn't enforce { ... } restriction on module
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
major
|
#16138 |
assertion failure when call tactic not given { ... } module restriction
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#16228 |
glob M computation problem with functors and inner modules for {*}
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#16231 |
General issues with computation of globals for nested modules
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
major
|
#16306 |
Bug in cloning ?
|
Benjamin Grégoire
|
defect
|
5
|
pre-1.x
|
major
|
#16362 |
Assertion failure when cloning a theory with let expressions
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
|
#16416 |
FEL completeness - initialization
|
Benjamin Grégoire
|
enhancement
|
3
|
pre-1.x
|
normal
|
#16622 |
Functor-level "lambdas"
|
Benjamin Grégoire
|
enhancement
|
2
|
pre-1.x
|
|
#16723 |
Subtyping for abstract modules and functors
|
Benjamin Grégoire
|
enhancement
|
3
|
pre-1.x
|
|
#16727 |
bd_hoare should work on >=, rather than forcing us to swap arguments
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
minor
|
#16729 |
Tactic swap causes inconsistent dependencies
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
blocker
|
#16732 |
Problem with functor aliases when outermost module is a parameter
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
|
#16749 |
link between hoare bdhoare equiv
|
Benjamin Grégoire
|
enhancement
|
3
|
pre-1.x
|
|
#16751 |
hoare should work on fun.
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#16787 |
new conseq issues
|
Benjamin Grégoire
|
defect
|
5
|
pre-1.x
|
blocker
|
#16849 |
Broken proc (in branch 1.0)
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
blocker
|
#16965 |
Non-termination when expanding a procedure whose body contains a generic projector (.`n)
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
critical
|
#17021 |
Some judgment-combining variants of conseq do not apply to procedures
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#17046 |
possible tactic renaming: [proc *] -> [eager proc *]
|
Benjamin Grégoire
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17083 |
Missing eta-reduction in conversion
|
Benjamin Grégoire
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17089 |
anomaly in [sim]
|
Benjamin Grégoire
|
defect
|
4
|
pre-1.x
|
normal
|
#17109 |
Hoare adversary rule introducess references to non-existent memories in postconditions
|
Benjamin Grégoire
|
defect
|
5
|
pre-1.x
|
normal
|
#17114 |
Unsoundness of module system
|
Benjamin Grégoire
|
defect
|
5
|
pre-1.x
|
blocker
|
#17128 |
assert false in rnd.
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#17129 |
bug in alias, the introduced variable has not the good type.
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#17130 |
"alias i" works only on random instruction.
|
Benjamin Grégoire
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17133 |
seq for phoare do not check the type of the arguments.
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#17142 |
Anomaly (related to SMT and memories)
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#17300 |
Module type checks have wrong variance when dealing with some functor configurations
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#17302 |
fel can generate subgoal with undefined memory
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#17303 |
more fel peculiarities
|
Benjamin Grégoire
|
defect
|
3
|
pre-1.x
|
normal
|
#17376 |
behaviour of module type include in functor types
|
Benjamin Grégoire
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17380 |
Internal "seq" of pHL tactics is unsound
|
Benjamin Grégoire
|
defect
|
5
|
pre-1.x
|
critical
|
#16103 |
scoping issue with theories
|
|
enhancement
|
3
|
pre-1.x
|
|
#16648 |
Make notations and tactics on distributions and functions a bit more uniform.
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#16912 |
Lifting the "collection update" statements to tuples
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#16987 |
Move facts from precondition to context
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17022 |
Pattern-matching on variables in judgments and probability expressions
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17036 |
Instantiating abstract modules: warnings and interactive justification
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#17045 |
Rewriting procedures in probability expressions directly from an equivalence
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#17086 |
Generalize [rewrite Pr]
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17090 |
Selecting procedure(s) to [inline] by position
|
|
enhancement
|
2
|
pre-1.x
|
normal
|
#17105 |
[transitivity] for phoare and hoare
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17113 |
Decide what to do on rewrite with defined head symbols
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17136 |
variant of seq to deal with large preconditions
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17140 |
Pattern matching should make use of simplification rules.
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17149 |
Expand glob A for concrete module
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17156 |
New vernacular command: `print axiom`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17163 |
Check that `phoare` tactics are forcing the input bounds to be in [0..1].
|
|
task
|
4
|
pre-1.x
|
major
|
#17164 |
behavior of -check-all
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17169 |
Anonymous functor arguments: passing procedures to functors directly
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17175 |
Direct intro on negative goals
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17183 |
Variant of `sim` that works modulo inlining.
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#17192 |
Problem with `glob` and type inference
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17197 |
Asserts in equivalence proofs
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17202 |
Add seq* tactic
|
|
enhancement
|
3
|
pre-1.x
|
major
|
#17210 |
Pattern-matching for pairs in operator arguments
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17215 |
Issues with module typing when functor parameters are themselves functors
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17217 |
need better error message when attempting to apply lemma to goal that isn't a judgment
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17218 |
proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17225 |
Explore reproducible smt calls
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17239 |
Mutual inductive types.
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17245 |
Formula manipulation commands (for `conseq` and `seq`)
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17246 |
`rewrite`, apply, ... in contracts
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17251 |
print Self
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17257 |
`/=` is too weak.
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17267 |
`auto` with `call`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17279 |
Improve `invalid goal shape` error messages for variants of `byequiv`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17281 |
Several problems with `apply` in program logics
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17282 |
call should not work
|
|
task
|
3
|
phl
|
normal
|
#17283 |
pattern matching complexity problem
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17285 |
Transitivity on procedures should support inferring contracts from `equiv` lemmas.
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17286 |
pRHL `apply` should have a framing variant
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17287 |
Program transformation tactics should not `anomaly` without a side in pRHL
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17288 |
EasyCrypt crashes when printing required abstract theory IterProc
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17290 |
`n!->>` should work
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17295 |
local ops
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17297 |
Allow the optional use of undeclared variables in procedures
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#17298 |
Super rnd
|
|
enhancement
|
4
|
phl
|
blocker
|
#17301 |
Applicative view for `if then else`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17305 |
proc* in eager case needlessly assigns result of procedures returning unit to variables
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17307 |
Coq style Locate
|
|
enhancement
|
1
|
pre-1.x
|
minor
|
#17311 |
`smt (@Self)`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17316 |
[smt (@Theory)] should force the use of axioms marked as `nosmt`
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17317 |
`search` should work somewhat better with abbreviations
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17322 |
use of side with HL version of while tactic should be syntax error
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17325 |
syntax marking end of cloning realization
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17337 |
substitutions should complain when substituting a locally defined variable
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17340 |
cfold should support variables (and more general terms).
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17341 |
for loops
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17342 |
Better support for rewriting with equivalences
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17344 |
Trees and polynomials
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17346 |
have access to notation in ml
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17348 |
Intro-pattern `|>` might transform a provable goal to a non-provable one
|
|
defect
|
3
|
pre-1.x
|
normal
|
(more results for this group on next page)
|