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

2 files changed, 34 insertions, 13 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 737e86848..8b78a91b5 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)
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0344dda97..20492e38c 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -980,6 +980,19 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
   else
     bind_termlist_env alp sigma x l
 
+let match_cast match_fun sigma c1 c2 =
+  match c1, c2 with
+  | CastConv t1, CastConv t2
+  | CastVM t1, CastVM t2
+  | CastNative t1, CastNative t2 ->
+    match_fun sigma t1 t2
+  | CastCoerce, CastCoerce ->
+    sigma
+  | CastConv _, _
+  | CastVM _, _
+  | CastNative _, _
+  | CastCoerce, _ -> 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 *)
   (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *)
@@ -1125,11 +1138,8 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let alp,sigma = Array.fold_right2 (fun id1 id2 alsig ->
 	match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
       Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
-  | GCast(c1,CastConv t1), NCast (c2,CastConv t2)
-  | GCast(c1,CastVM t1), NCast (c2,CastVM t2) ->
-      match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
-  | GCast(c1, CastCoerce), NCast(c2, CastCoerce) ->
-      match_in u alp metas sigma c1 c2
+  | GCast(t1, c1), NCast(t2, c2) ->
+    match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
   | GSort (GType _), NSort (GType _) when not u -> sigma
   | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
@@ -1157,8 +1167,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
 
-  | (GRec _ | GEvar _), _
-  | _,_ -> raise No_match
+  | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
+     | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
+     | GCast _), _ -> raise No_match
 
 and match_in u = match_ true u