| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations
no longer modify the parser in non-compat-mode, so we can do this
without breaking Ltac parsing. Also update the related test-suite
files.
|
|
|
|
|
|
|
|
We add a flag Keep Admitted Variables that allows to recover the legacy
v8.4 behaviour of admitted lemmas. The statement of such lemmas did not
depend on the current context variables.
|
|
|
|
We don't actually need to, unless we want to support the (presumably
uncommon) use-case of someone using [Import VectorNotations] to override
their local notation for things in vector_scope.
Additionally, we now maintain the behavior that [Import VectorNotations]
opens vector_scope.
|
|
With this commit, it is possible to write notations so that singleton
lists are usable in both 8.4 and 8.5pl1 -compat. Longer lists await the
ability to remove notations from the parser.
|
|
|
|
and global for 8.4 and 8.5.
|
|
|
|
|
|
there is actually no change in default subst between 8.4 and 8.5.
|
|
into v8.5
|
|
|
|
Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in
8.4.
|
|
I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd;
Coq.Init.Notations.constructor does not take any arguments.
|
|
We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit.
|
|
|
|
|
|
Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4.
|
|
|
|
|
|
Now doing
```coq
Tactic Notation "left" "~" := left.
Tactic Notation "left" "*" := left.
```
will no longer break the `left` tactic in Coq 8.4.
List obtained via
```
grep -o '^ \[[^]]*\]' tactics/coretactics.ml4 | sed s'/^ \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g'
```
|
|
|
