diff options
| author | Pierre-Marie Pédrot | 2015-11-05 16:34:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-05 16:34:37 +0100 |
| commit | 55a765faa95d7be9a1e4c37096139f57f288f55a (patch) | |
| tree | 459ac71b1478d69f77f8663c1001c10ca0ae528d /theories | |
| parent | 35afb42a6bb30634d2eb77a32002ed473633b5f4 (diff) | |
| parent | 0fd6ad21121c7c179375b9a50c3135abab1781b2 (diff) | |
Merge branch 'v8.5'
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 83016976e8..b04d5168f2 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. *) |