diff options
| -rw-r--r-- | theories/Compat/Coq84.v | 8 |
1 files changed, 8 insertions, 0 deletions
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. |