diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-04-07 15:58:58 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-04-07 16:14:20 +0200 |
| commit | f6a8ce665815af9609163198f609e1db8ca49b47 (patch) | |
| tree | c8e17a35055a6159b7bda326d8d06175dc422f95 /theories/Compat/Coq84.v | |
| parent | f9ef1441083a988a938e163393dfbab04ab9da18 (diff) | |
| parent | ab08345ebdb477bf4c83b46e0d8adc29296392f9 (diff) | |
Merge PR#152: Add -compat 8.4 econstructor tactics, and tests
Diffstat (limited to 'theories/Compat/Coq84.v')
| -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. |