From ab08345ebdb477bf4c83b46e0d8adc29296392f9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 5 Apr 2016 13:18:00 -0400 Subject: Add -compat 8.4 econstructor tactics, and tests Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in 8.4. --- theories/Compat/Coq84.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'theories/Compat/Coq84.v') 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. -- cgit v1.2.3