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