diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-04-05 13:18:00 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-04-05 13:19:07 -0400 |
| commit | ab08345ebdb477bf4c83b46e0d8adc29296392f9 (patch) | |
| tree | dde496b7f0e4b87fa239692ae6f5b142c8d0238c /theories/Compat | |
| parent | a585d46fbacfcc9cddf3da439e5f7001d429ba2a (diff) | |
Add -compat 8.4 econstructor tactics, and tests
Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in
8.4.
Diffstat (limited to 'theories/Compat')
| -rw-r--r-- | theories/Compat/Coq84.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 326628192..d99d50996 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -29,6 +29,14 @@ Tactic Notation "constructor" := Coq.Init.Notations.constructor. Tactic Notation "constructor" int_or_var(n) := constructor_84_n n. Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac. +(** In 8.4, [econstructor (tac)] allowed backtracking across the use of [econstructor]; it has been subsumed by [econstructor; tac]. *) +Ltac econstructor_84_n n := econstructor n. +Ltac econstructor_84_tac tac := once (econstructor; tac). + +Tactic Notation "econstructor" := Coq.Init.Notations.econstructor. +Tactic Notation "econstructor" int_or_var(n) := econstructor_84_n n. +Tactic Notation "econstructor" "(" tactic(tac) ")" := econstructor_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. @@ -44,7 +52,6 @@ Tactic Notation "left" := left. Tactic Notation "eleft" := eleft. Tactic Notation "right" := right. Tactic Notation "eright" := eright. -Tactic Notation "econstructor" := econstructor. Tactic Notation "symmetry" := symmetry. Tactic Notation "split" := split. Tactic Notation "esplit" := esplit. |