diff options
Diffstat (limited to 'theories/Compat')
| -rw-r--r-- | theories/Compat/AdmitAxiom.v | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq84.v | 47 | ||||
| -rw-r--r-- | theories/Compat/Coq85.v | 2 |
3 files changed, 23 insertions, 28 deletions
diff --git a/theories/Compat/AdmitAxiom.v b/theories/Compat/AdmitAxiom.v index 68607f6b2..4d9f55cfe 100644 --- a/theories/Compat/AdmitAxiom.v +++ b/theories/Compat/AdmitAxiom.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 729687636..39bc59a65 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,21 +19,28 @@ 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. -(** 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" := 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. @@ -49,29 +56,17 @@ 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. *) -Require Coq.ZArith.Int. -Module Export Coq. - Module Export ZArith. - Module Int. - Module Z_as_Int. - Include Coq.ZArith.Int.Z_as_Int. - (* FIXME: Should these get a (compat "8.4")? Or be moved to Z_as_Int, probably? *) - Notation plus := Coq.ZArith.Int.Z_as_Int.add (only parsing). - Notation minus := Coq.ZArith.Int.Z_as_Int.sub (only parsing). - Notation mult := Coq.ZArith.Int.Z_as_Int.mul (only parsing). - End Z_as_Int. - End Int. - End ZArith. -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. diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 7ce04a662..af2e04f88 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |