Merge PR #13911: Remove the :> type cast?

Reviewed-by: mattam82
Ack-by: Zimmi48

3 files changed, 3 insertions, 10 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 86d2cc78e0..5a8ac32ffa 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -104,9 +104,8 @@ let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
 let cast_type_eq eq t1 t2 = match t1, t2 with
   | CastConv t1, CastConv t2 -> eq t1 t2
   | CastVM t1, CastVM t2 -> eq t1 t2
-  | CastCoerce, CastCoerce -> true
   | CastNative t1, CastNative t2 -> eq t1 t2
-  | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false
+  | (CastConv _ | CastVM _ | CastNative _), _ -> false
 
 let matching_var_kind_eq k1 k2 = match k1, k2 with
 | FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2
@@ -188,14 +187,12 @@ let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 let map_cast_type f = function
   | CastConv a -> CastConv (f a)
   | CastVM a -> CastVM (f a)
-  | CastCoerce -> CastCoerce
   | CastNative a -> CastNative (f a)
 
 let smartmap_cast_type f c =
   match c with
     | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
     | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
-    | CastCoerce -> CastCoerce
     | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
 
 let map_glob_constr_left_to_right f = DAst.map (function
@@ -275,7 +272,7 @@ let fold_glob_constr f acc = DAst.with_val (function
     Array.fold_left f (Array.fold_left f acc tyl) bv
   | GCast (c,k) ->
     let acc = match k with
-      | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
+      | CastConv t | CastVM t | CastNative t -> f acc t in
     f acc c
   | GArray (_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc
@@ -318,7 +315,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
     Array.fold_left_i f' acc idl
   | GCast (c,k) ->
     let acc = match k with
-      | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
+      | CastConv t | CastVM t | CastNative t -> f v acc t in
     f v acc c
   | GArray (_u, t, def, ty) -> f v (f v (Array.fold_left (f v) acc t) def) ty
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc))
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 9f93e5e6c1..d480c12834 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -57,7 +57,6 @@ and glob_fix_kind =
 type 'a cast_type =
   | CastConv of 'a
   | CastVM of 'a
-  | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
   | CastNative of 'a
 
 (**  The kind of patterns that occurs in "match ... with ... end"
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 21b2137f09..4c2fc26b45 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1166,9 +1166,6 @@ struct
     let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in
     let sigma, cj =
       match k with
-      | CastCoerce ->
-        let sigma, cj = pretype empty_tycon env sigma c in
-        Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj
       | CastConv t | CastVM t | CastNative t ->
         let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
         let sigma, tj = eval_type_pretyper self ~program_mode ~poly resolve_tc empty_valcon env sigma t in