No more Coersion in Init.

3 files changed, 15 insertions, 23 deletions

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index d1c567bec..f58c21f48 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -85,7 +85,7 @@ End Subset_projections.
 
 (** [sig2] of a predicate can be projected to a [sig].
 
-    This allows [proj1_sig] and [proj2_sig] to work with [sig2].
+    This allows [proj1_sig] and [proj2_sig] to be usable with [sig2].
 
     The [let] statements occur in the body of the [exist] so that
     [proj1_sig] of a coerced [X : sig2 P Q] will unify with [let (a,
@@ -96,14 +96,13 @@ Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P
            (let (a, _, _) := X in a)
            (let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p).
 
-Coercion sig_of_sig2 : sig2 >-> sig.
-
 (** Projections of [sig2]
 
     An element [y] of a subset [{x:A | (P x) & (Q x)}] is the triple
     of an [a] of type [A], a of a proof [h] that [a] satisfies [P],
-    and a proof [h'] that [a] satisfies [Q].  Then [(proj1_sig y)] is
-    the witness [a], [(proj2_sig y)] is the proof of [(P a)], and
+    and a proof [h'] that [a] satisfies [Q].  Then
+    [(proj1_sig (sig_of_sig2 y))] is the witness [a],
+    [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and 
     [(proj3_sig y)] is the proof of [(Q a)]. *)
 
 Section Subset_projections2.
@@ -112,7 +111,7 @@ Section Subset_projections2.
   Variables P Q : A -> Prop.
 
   Definition proj3_sig (e : sig2 P Q) :=
-    let (a, b, c) return Q (proj1_sig e) := e in c.
+    let (a, b, c) return Q (proj1_sig (sig_of_sig2 e)) := e in c.
 
 End Subset_projections2.
 
@@ -141,7 +140,7 @@ End Projections.
 
 (** [sigT2] of a predicate can be projected to a [sigT].
 
-    This allows [projT1] and [projT2] to work with [sigT2].
+    This allows [projT1] and [projT2] to be usable with [sigT2].
 
     The [let] statements occur in the body of the [existT] so that
     [projT1] of a coerced [X : sigT2 P Q] will unify with [let (a,
@@ -152,15 +151,14 @@ Definition sigT_of_sigT2 (A : Type) (P Q : A -> Type) (X : sigT2 P Q) : sigT P
             (let (a, _, _) := X in a)
             (let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p).
 
-Coercion sigT_of_sigT2 : sigT2 >-> sigT.
-
 (** Projections of [sigT2]
 
     An element [x] of a sigma-type [{y:A & P y & Q y}] is a dependent
     pair made of an [a] of type [A], an [h] of type [P a], and an [h']
-    of type [Q a].  Then, [(projT1 x)] is the first projection,
-    [(projT2 x)] is the second projection, and [(projT3 x)] is the
-    third projection, the types of which depends on the [projT1]. *)
+    of type [Q a].  Then, [(projT1 (sigT_of_sigT2 x))] is the first
+    projection, [(projT2 (sigT_of_sigT2 x))] is the second projection,
+    and [(projT3 x)] is the third projection, the types of which
+    depends on the [projT1]. *)
 
 Section Projections2.
 
@@ -168,7 +166,7 @@ Section Projections2.
   Variables P Q : A -> Type.
 
   Definition projT3 (e : sigT2 P Q) :=
-    let (a, b, c) return Q (projT1 e) := e in c.
+    let (a, b, c) return Q (projT1 (sigT_of_sigT2 e)) := e in c.
 
 End Projections2.
 
@@ -180,19 +178,13 @@ Definition sig_of_sigT (A : Type) (P : A -> Prop) (X : sigT P) : sig P
 Definition sigT_of_sig (A : Type) (P : A -> Prop) (X : sig P) : sigT P
   := existT P (proj1_sig X) (proj2_sig X).
 
-Coercion sigT_of_sig : sig >-> sigT.
-Coercion sig_of_sigT : sigT >-> sig.
-
 (** [sigT2] of a predicate is equivalent to [sig2] *)
 
 Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q
-  := exist2 P Q (projT1 X) (projT2 X) (projT3 X).
+  := exist2 P Q (projT1 (sigT_of_sigT2 X)) (projT2 (sigT_of_sigT2 X)) (projT3 X).
 
 Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q
-  := existT2 P Q (proj1_sig X) (proj2_sig X) (proj3_sig X).
-
-Coercion sigT2_of_sig2 : sig2 >-> sigT2.
-Coercion sig2_of_sigT2 : sigT2 >-> sig2.
+  := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X).
 
 (** [sumbool] is a boolean type equipped with the justification of
     their value *)
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index a5e4f8f7e..328ba27e6 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -261,7 +261,7 @@ Section sequence.
   Lemma Un_cv_crit : Un_growing -> bound EUn ->  exists l : R, Un_cv l.
   Proof.
     intros Hug Heub.
-    exists (projT1 (completeness EUn Heub EUn_noempty)).
+    exists (proj1_sig (completeness EUn Heub EUn_noempty)).
     destruct (completeness EUn Heub EUn_noempty) as (l, H).
     now apply Un_cv_crit_lub.
   Qed.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 5254ff2cc..52657b401 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -27,7 +27,7 @@ Lemma growing_cv :
   forall Un:nat -> R, Un_growing Un -> has_ub Un -> { l:R | Un_cv Un l }.
 Proof.
   intros Un Hug Heub.
-  exists (projT1 (completeness (EUn Un) Heub (EUn_noempty Un))).
+  exists (proj1_sig (completeness (EUn Un) Heub (EUn_noempty Un))).
   destruct (completeness _ Heub (EUn_noempty Un)) as (l, H).
   now apply Un_cv_crit_lub.
 Qed.