From 59cb5ca9b6c0e29fe65e9ae99dfd6cabafc52be6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 28 Oct 2015 15:17:30 -0400 Subject: Add compatibility Nonrecursive Elimination Schemes --- theories/Compat/Coq84.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'theories/Compat') diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 90083b00d..d695ef1d8 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -15,6 +15,9 @@ Ltac omega := Coq.omega.Omega.omega. (** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *) Global Set Asymmetric Patterns. +(** The automatic elimination schemes for records were dropped by default in 8.5. This restores the default behavior of Coq 8.4. *) +Global Set Nonrecursive Elimination Schemes. + (** See bug 3545 *) Global Set Universal Lemma Under Conjunction. -- cgit v1.2.3 From 4c078b0362542908eb2fe1d63f0d867b339953fd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 29 Dec 2015 13:21:17 -0500 Subject: Update Coq84.v We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit. --- theories/Compat/Coq84.v | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'theories/Compat') diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index d695ef1d8..5036b9bc8 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -21,16 +21,11 @@ Global Set Nonrecursive Elimination Schemes. (** See bug 3545 *) Global Set Universal Lemma Under Conjunction. -(** In 8.5, [refine] leaves over dependent subgoals. *) -Tactic Notation "refine" uconstr(term) := refine term; shelve_unifiable. - (** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *) -Ltac constructor_84 := constructor. -Ltac constructor_84_n n := constructor n. Ltac constructor_84_tac tac := once (constructor; tac). -Tactic Notation "constructor" := constructor_84. -Tactic Notation "constructor" int_or_var(n) := constructor_84_n n. +Tactic Notation "constructor" := Coq.Init.Notations.constructor. +Tactic Notation "constructor" int_or_var(n) := Coq.Init.Notations.constructor 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. *) -- cgit v1.2.3 From a585d46fbacfcc9cddf3da439e5f7001d429ba2a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 5 Apr 2016 12:56:52 -0400 Subject: Fix bug #4656 I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd; Coq.Init.Notations.constructor does not take any arguments. --- test-suite/bugs/closed/4656.v | 4 ++++ theories/Compat/Coq84.v | 4 ++-- 2 files changed, 6 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/4656.v (limited to 'theories/Compat') diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v new file mode 100644 index 000000000..c89a86d63 --- /dev/null +++ b/test-suite/bugs/closed/4656.v @@ -0,0 +1,4 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +Goal True. + constructor 1. +Qed. diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 5036b9bc8..326628192 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -22,10 +22,11 @@ Global Set Nonrecursive Elimination Schemes. Global Set Universal Lemma Under Conjunction. (** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *) +Ltac constructor_84_n n := constructor n. Ltac constructor_84_tac tac := once (constructor; tac). Tactic Notation "constructor" := Coq.Init.Notations.constructor. -Tactic Notation "constructor" int_or_var(n) := Coq.Init.Notations.constructor n. +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. *) @@ -43,7 +44,6 @@ 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. -- cgit v1.2.3 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. --- test-suite/success/Compat84.v | 19 +++++++++++++++++++ theories/Compat/Coq84.v | 9 ++++++++- 2 files changed, 27 insertions(+), 1 deletion(-) create mode 100644 test-suite/success/Compat84.v (limited to 'theories/Compat') diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v new file mode 100644 index 000000000..db6348fa1 --- /dev/null +++ b/test-suite/success/Compat84.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) + +Goal True. + solve [ constructor 1 ]. Undo. + solve [ econstructor 1 ]. Undo. + solve [ constructor ]. Undo. + solve [ econstructor ]. Undo. + solve [ constructor (fail) ]. Undo. + solve [ econstructor (fail) ]. Undo. + split. +Qed. + +Goal False \/ True. + solve [ constructor (constructor) ]. Undo. + solve [ econstructor (econstructor) ]. Undo. + solve [ constructor 2; constructor ]. Undo. + solve [ econstructor 2; econstructor ]. Undo. + right; esplit. +Qed. 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 From 84f079fa31723b6a97edc50ca7a81e1eb19e759c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 7 Apr 2016 20:31:42 +0200 Subject: Added compatibility coercions from Specif.v which were present in Coq 8.4. --- theories/Compat/Coq84.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'theories/Compat') diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index d99d50996..5c60966f2 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -76,3 +76,11 @@ End Coq. (** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *) Require Coq.Numbers.Natural.Peano.NPeano. + +(** The following coercions were declared by default in Specif.v. *) +Coercion sig_of_sig2 : sig2 >-> sig. +Coercion sigT_of_sigT2 : sigT2 >-> sigT. +Coercion sigT_of_sig : sig >-> sigT. +Coercion sig_of_sigT : sigT >-> sig. +Coercion sigT2_of_sig2 : sig2 >-> sigT2. +Coercion sig2_of_sigT2 : sigT2 >-> sig2. -- cgit v1.2.3