#17144 
Module type checking: Unclear error message and probably bug

PierreYves Strub

defect

3

pre1.x

normal

#17145 
"choice" reorders its arguments

PierreYves Strub

defect

3

pre1.x

normal

#17146 
Bad error message in combination choice/modules/section

PierreYves Strub

defect

3

pre1.x

normal

#17147 
Parse error in (some) expressions involving memories

PierreYves Strub

defect

3

pre1.x

normal

#17151 
Abstract theories

PierreYves Strub

enhancement

3

pre1.x

normal

#17153 
seq does not check type of its arguments

PierreYves Strub

defect

3

pre1.x

normal

#17154 
anomaly: EcPV.MemoryClash


defect

3

pre1.x

normal

#17158 
"<" for predicates when cloning

PierreYves Strub

enhancement

3

pre1.x

normal

#17159 
expect should support goal selection

PierreYves Strub

enhancement

3

pre1.x

normal

#17162 
Bad interaction between abstract theories and local modules

PierreYves Strub

defect

4

pre1.x

normal

#17165 
nottobeproved lemmas

PierreYves Strub

enhancement

3

pre1.x

normal

#17166 
missing syntax for proving all axioms of a theory, its subtheories, etc., when cloning

PierreYves Strub

enhancement

3

pre1.x

normal

#17167 
Better localization of errors when typing a proofterm

PierreYves Strub

enhancement

3

pre1.x

normal

#17170 
Introduce theory for product distribution

PierreYves Strub

enhancement

3

pre1.x

normal

#17171 
mode similar to nocheck that tries smt calls and just prints the locations for the failing calls

PierreYves Strub

enhancement

3

pre1.x

normal

#17172 
Looping on `rewrite !/op`

PierreYves Strub

defect

3

pre1.x

normal

#17173 
alternative to "require A; clone export A as B" that does not add A to SMT context


enhancement

3

pre1.x

normal

#17174 
Return of the memory explosion


defect

3

pre1.x

normal

#17176 
[print] should display types even on fixpoints

PierreYves Strub

enhancement

3

pre1.x

normal

#17178 
Generalizing over an empty list should generate a sane name

PierreYves Strub

defect

3

pre1.x

normal

#17179 
`done` should close goals with a direct contradiction in its env.

PierreYves Strub

enhancement

3

pre1.x

normal

#17180 
anomaly: File "src/ecCoreFol.ml", line 1207, characters 1925: Assertion failed

PierreYves Strub

defect

3

pre1.x

normal

#17184 
parse error involving parameterized module

PierreYves Strub

defect

3

pre1.x

normal

#17187 
anomaly when invalid memory is referenced  should be proper error message

PierreYves Strub

defect

3

pre1.x

normal

#17188 
Error with smt : lazy


defect

3

pre1.x

normal

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

PierreYves Strub

enhancement

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17191 
Assert failure

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17196 
Vernacular command for dumping env. as a Why3 task.

PierreYves Strub

enhancement

3

pre1.x

normal

#17198 
Spurious failure of rewrite

PierreYves Strub

defect

3

pre1.x

normal

#17201 
`xy` and `x + y` should be convertible

PierreYves Strub

enhancement

3

pre1.x

normal

#17203 
Rewrite strangely failling

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

enhancement

1

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17206 
Missing parens in the pretty printer

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17211 
split causes anomaly when given equality between constructors

PierreYves Strub

defect

3

pre1.x

normal

#17212 
Circular [require] dependencies should be caught instead of blowing up computers

PierreYves Strub

defect

3

pre1.x

normal

#17214 
Wrong printed for memory

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

enhancement

3

pre1.x

normal

#17221 
parsing change allowing lemma ... by tactics

PierreYves Strub

enhancement

3

pre1.x

normal

#17223 
use of ' and ` in operator names causes anomaly rather than error message

PierreYves Strub

defect

3

pre1.x

normal

#17224 
type declarations with bad type variables yield anomalies rather than error messages

PierreYves Strub

defect

3

pre1.x

normal

#17226 
some weirdness with operators of form :+

PierreYves Strub

defect

3

pre1.x

normal

#17228 
pretty printer uses bad syntax for type constructors

PierreYves Strub

defect

3

pre1.x

normal

#17229 
pretty printer errors with inductive datatypes

PierreYves Strub

defect

3

pre1.x

normal

#17230 
unhelpful error message when there are two matching operators with needed type

PierreYves Strub

enhancement

3

pre1.x

normal

#17231 
check for datatype being inhabited isn't complete, but error message suggests it is

PierreYves Strub

enhancement

3

pre1.x

normal

#17232 
weirdness involving redefining (=) or defining (<>)


enhancement

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17234 
Allow omission of a procedure's return type when it can be inferred

PierreYves Strub

enhancement

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17236 
error with rewriting occurrence of 1 when only one matching occurrence


defect

3

pre1.x

normal

#17237 
failure of rewrite ... in ...

PierreYves Strub

defect

3

pre1.x

normal

#17238 
anomaly with autorevert intro pattern

PierreYves Strub

defect

3

pre1.x

normal

#17241 
`clone import` not working when realizing axioms.

PierreYves Strub

defect

3

pre1.x

normal

#17242 
`print` should display `nosmt` info

PierreYves Strub

enhancement

3

pre1.x

normal

#17243 
Internal error (anomaly) on proof script

PierreYves Strub

defect

3

pre1.x

normal

#17244 
Imprecise "uninitialized local variables" warning

PierreYves Strub

defect

3

pre1.x

normal

#17247 
Interactive proof realisation for `instance`

PierreYves Strub

enhancement

3

pre1.x

normal

#17248 
More precise error messages when noninteractive realization fails

PierreYves Strub

enhancement

3

pre1.x

normal

#17249 
`AlgTactic` && `Ring` should agree on their axioms.

PierreYves Strub

enhancement

2

pre1.x

normal

#17254 
print produces misleading results on partially applied functors


defect

3

pre1.x

normal

#17258 
Intro pattern for hypothesis duplication

PierreYves Strub

enhancement

3

pre1.x

normal

#17260 
pragma +option should fail gracefully.

PierreYves Strub

defect

3

pre1.x

normal

#17269 
Add notations for >/>=

PierreYves Strub

enhancement

3

pre1.x

normal

#17270 
`done` should close a goal when `false` is a local hyp.

PierreYves Strub

enhancement

5

pre1.x

normal

#17275 
[congr] should apply to iff

PierreYves Strub

defect

3

pre1.x

normal

#17276 
the pretty printer is getting the relative precedences of unary  and %% wrong

PierreYves Strub

defect

3

pre1.x

normal

#17277 
Higherorder patternmatching with quantifiers

PierreYves Strub

defect

3

pre1.x

normal

#17278 
[eta] reduction is not full on multiary functions

github <noreply@…>

defect

3

pre1.x

normal

#17280 
Parseonly abbreviations

PierreYves Strub

enhancement

3

pre1.x

normal

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

PierreYves Strub

enhancement

3

pre1.x

normal

#17289 
Missing dependencies in OPAM package


defect

3

pre1.x

normal

#17290 
`n!>>` should work


enhancement

3

pre1.x

normal

#17291 
`move: x` should keep the body of `x` if any.

PierreYves Strub

defect

3

pre1.x

normal

#17292 
anomaly on application of a `<=>` lemma to a `=` goal


defect

3

pre1.x

normal

#17293 
Looping behaviour in reduction/simplification. Probably related to reals.

PierreYves Strub

defect

3

pre1.x

normal

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


defect

3

pre1.x

normal

#17299 
Transitivity using an equiv


enhancement

3

phl

normal

#17300 
Module type checks have wrong variance when dealing with some functor configurations

Benjamin Grégoire

defect

3

pre1.x

normal

#17302 
fel can generate subgoal with undefined memory

Benjamin Grégoire

defect

3

pre1.x

normal

#17303 
more fel peculiarities

Benjamin Grégoire

defect

3

pre1.x

normal

#17304 
Regression on anonymous procedure arguments support

PierreYves Strub

defect

3

pre1.x

normal

#17306 
Operator folding and unfolding not checking type parameters

PierreYves Strub

defect

3

pre1.x

normal

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

PierreYves Strub

defect

3

pre1.x

normal

#17312 
cloning can create illformed definitions

PierreYves Strub

defect

3

pre1.x

normal

#17313 
module types with multiple occurrences of same procedure should not be accepted

PierreYves Strub

defect

3

pre1.x

normal

#17314 
Syntax variants of multiple argument module types don't match ones for parameterized modules

PierreYves Strub

enhancement

3

pre1.x

normal

#17315 
[print] on notations is not very useful


defect

3

pre1.x

normal

#17317 
`search` should work somewhat better with abbreviations

PierreYves Strub

enhancement

3

pre1.x

normal

#17318 
clonetime regexp substitution should apply in the specified order

PierreYves Strub

defect

3

pre1.x

normal

#17320 
anomaly when cloning theory with inductive predicate

PierreYves Strub

defect

3

pre1.x

normal

#17323 
> ip anomaly

PierreYves Strub

defect

3

pre1.x

normal

#17324 
> ip expands predicates in conclusion

PierreYves Strub

defect

3

pre1.x

normal

#17326 
`+` intropattern may reorder assumptions

PierreYves Strub

defect

3

pre1.x

normal

#17327 
Variants of `<*>` with preference

PierreYves Strub

enhancement

3

pre1.x

normal

#17328 
`_` intropattern should only check if the clear is possible once the rest of the intropattern has been processed


enhancement

3

pre1.x

normal

(more results for this group on next page)
