diff options
Diffstat (limited to 'theories')
| -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. *) |