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

Reviewed-by: mattam82
Ack-by: Zimmi48

2 files changed, 3 insertions, 10 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index f02874253e..40fe13784a 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -261,11 +261,9 @@ and cast_expr_eq c1 c2 = match c1, c2 with
 | CastConv t1, CastConv t2
 | CastVM t1, CastVM t2
 | CastNative t1, CastNative t2 -> constr_expr_eq t1 t2
-| CastCoerce, CastCoerce -> true
 | CastConv _, _
 | CastVM _, _
-| CastNative _, _
-| CastCoerce, _ -> false
+| CastNative _, _ -> false
 
 let constr_loc c = CAst.(c.loc)
 let cases_pattern_expr_loc cp = CAst.(cp.loc)
@@ -343,7 +341,6 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
     | CLetIn (na,a,t,b) ->
       f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
     | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
-    | CCast (a,CastCoerce) -> f n acc a
     | CNotation (_,_,(l,ll,bl,bll)) ->
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ea5e2a1ad4..ea95655c18 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -35,9 +35,8 @@ let rec alpha_var id1 id2 = function
 let cast_type_iter2 f t1 t2 = match t1, t2 with
   | CastConv t1, CastConv t2 -> f t1 t2
   | CastVM t1, CastVM t2 -> f t1 t2
-  | CastCoerce, CastCoerce -> ()
   | CastNative t1, CastNative t2 -> f t1 t2
-  | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit
+  | (CastConv _ | CastVM _ | CastNative _), _ -> raise Exit
 
 (* used to update the notation variable with the local variables used
    in NList and NBinderList, since the iterator has its own variable *)
@@ -1319,12 +1318,9 @@ let match_cast match_fun sigma c1 c2 =
   | CastVM t1, CastVM t2
   | CastNative t1, CastNative t2 ->
     match_fun sigma t1 t2
-  | CastCoerce, CastCoerce ->
-    sigma
   | CastConv _, _
   | CastVM _, _
-  | CastNative _, _
-  | CastCoerce, _ -> raise No_match
+  | CastNative _, _ -> raise No_match
 
 let does_not_come_from_already_eta_expanded_var glob =
   (* This is hack to avoid looping on a rule with rhs of the form *)