Merge PR #486: Make some functions on terms more robust w.r.t new term constructs.

1 files changed, 16 insertions, 6 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 737e86848c..8b78a91b5b 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -159,11 +159,8 @@ let rec constr_expr_eq e1 e2 =
       Id.equal id1 id2 && List.equal instance_eq c1 c2
     | CSort s1, CSort s2 ->
       Miscops.glob_sort_eq s1 s2
-    | CCast(a1,(CastConv b1|CastVM b1)), CCast(a2,(CastConv b2|CastVM b2)) ->
-      constr_expr_eq a1 a2 &&
-      constr_expr_eq b1 b2
-    | CCast(a1,CastCoerce), CCast(a2, CastCoerce) ->
-      constr_expr_eq a1 a2
+  | CCast(t1,c1), CCast(t2,c2) ->
+    constr_expr_eq t1 t2 && cast_expr_eq c1 c2
     | CNotation(n1, s1), CNotation(n2, s2) ->
       String.equal n1 n2 &&
       constr_notation_substitution_eq s1 s2
@@ -176,7 +173,10 @@ let rec constr_expr_eq e1 e2 =
     | CDelimiters(s1,e1), CDelimiters(s2,e2) ->
       String.equal s1 s2 &&
       constr_expr_eq e1 e2
-    | _ -> false
+  | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
+     | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
+     | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
+     | CGeneralization _ | CDelimiters _), _ -> false
 
 and args_eq (a1,e1) (a2,e2) =
   Option.equal (eq_located explicitation_eq) e1 e2 &&
@@ -232,6 +232,16 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
 and instance_eq (x1,c1) (x2,c2) =
   Id.equal x1 x2 && constr_expr_eq c1 c2
 
+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
+
 let constr_loc c = CAst.(c.loc)
 let cases_pattern_expr_loc cp = CAst.(cp.loc)