diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2015-10-30 13:32:42 -0400 |
|---|---|---|
| committer |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-03 11:55:52 +0100 |
| commit | 5f8f9e5b8eb22a413090229bc317fc2f36c053ac (patch) | |
| tree | 291ddb2988a9ef20c811b0154f4dd51203703836 | |
| parent | dc65d720f3928fd987f82e1571521b52844dd248 (diff) | |
Update compatibility file for some of bug #4392
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'
```
| -rw-r--r-- | theories/Compat/Coq84.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 83016976e..b04d5168f 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -34,6 +34,27 @@ Tactic Notation "constructor" := constructor_84. Tactic Notation "constructor" int_or_var(n) := constructor_84_n n. Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac. +(** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *) +Tactic Notation "reflexivity" := reflexivity. +Tactic Notation "assumption" := assumption. +Tactic Notation "etransitivity" := etransitivity. +Tactic Notation "cut" constr(c) := cut c. +Tactic Notation "exact_no_check" constr(c) := exact_no_check c. +Tactic Notation "vm_cast_no_check" constr(c) := vm_cast_no_check c. +Tactic Notation "casetype" constr(c) := casetype c. +Tactic Notation "elimtype" constr(c) := elimtype c. +Tactic Notation "lapply" constr(c) := lapply c. +Tactic Notation "transitivity" constr(c) := transitivity c. +Tactic Notation "left" := left. +Tactic Notation "eleft" := eleft. +Tactic Notation "right" := right. +Tactic Notation "eright" := eright. +Tactic Notation "constructor" := constructor. +Tactic Notation "econstructor" := econstructor. +Tactic Notation "symmetry" := symmetry. +Tactic Notation "split" := split. +Tactic Notation "esplit" := esplit. + Global Set Regular Subst Tactic. (** Some names have changed in the standard library, so we add aliases. *) |