diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-07 20:31:42 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-04-08 15:48:32 +0200 |
| commit | 84f079fa31723b6a97edc50ca7a81e1eb19e759c (patch) | |
| tree | f11050de4cee8946658849bf2173bba0239776c5 /theories/Compat | |
| parent | 17c9a9775e99d1551bf6d346d731271e3ae34417 (diff) | |
Added compatibility coercions from Specif.v which were present in Coq 8.4.
Diffstat (limited to 'theories/Compat')
| -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. |