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

4 files changed, 29 insertions, 11 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 3a9179813..20ef65c88 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -371,7 +371,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
       |	PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst
       | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
          Array.fold_left2 (sorec ctx env) subst args1 args2
-      | _ -> raise PatternMatchingFailure
+      | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
+         | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _
+         | PFix _ | PCoFix _| PEvar _), _ -> raise PatternMatchingFailure
 
   in
   sorec [] env (Id.Map.empty, Id.Map.empty) pat c
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 4d8c09c50..41e09004c 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -59,7 +59,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
   fixpoint_eq f1 f2
 | PCoFix f1, PCoFix f2 ->
   cofixpoint_eq f1 f2
-| _ -> false
+| PProj (p1, t1), PProj (p2, t2) ->
+   Projection.equal p1 p2 && constr_pattern_eq t1 t2
+| (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
+   | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _
+   | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _), _ -> false
 (** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
 
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
@@ -442,8 +446,8 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
 	 one non-trivial branch. These facts are used in [Constrextern]. *)
       PCase (info, pred, pat_of_raw metas vars c, brs)
 
-  | r -> err ?loc (Pp.str "Non supported pattern.")
-  )
+  | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
+      err ?loc (Pp.str "Non supported pattern."))
 
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg p = match DAst.get p with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 04374c88b..ba0502ca4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1167,7 +1167,8 @@ let local_whd_state_gen flags sigma =
 	|_ -> s
       else s
 
-    | x -> s
+    | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _  | Ind _ | Proj _ -> s
+
   in
   whrec
 
@@ -1771,8 +1772,8 @@ let meta_reducible_instance evd b =
           let is_coerce = match s with CoerceToType -> true | _ -> false in
           if not is_coerce then irec g else u
 	 with Not_found -> u)
-    | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) ->
-	let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) in
+    | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) ->
+      let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
 	  (match
 	  try
 	    let g, s = Metamap.find m metas in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a4e2f90d4..84ffab426 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -573,7 +573,9 @@ let is_rigid_head sigma flags t =
   | Ind (i,u) -> true
   | Construct _ -> true
   | Fix _ | CoFix _ -> true
-  | _ -> false
+  | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod (_, _, _)
+    | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _)
+    | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
 
 let force_eqs c = 
   Universes.Constraints.fold
@@ -654,7 +656,10 @@ let rec is_neutral env sigma ts t =
     | Evar _ | Meta _ -> true
     | Case (_, p, c, cl) -> is_neutral env sigma ts c
     | Proj (p, c) -> is_neutral env sigma ts c
-    | _ -> false
+    | Lambda _ | LetIn _ | Construct _ | CoFix _ -> false
+    | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
+    | Fix _ -> false (* This is an approximation *)
+    | App _ -> assert false
 
 let is_eta_constructor_app env sigma ts f l1 term =
   match EConstr.kind sigma f with
@@ -1788,7 +1793,9 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
 
-          | _ -> user_err Pp.(str "Match_subterm")))
+          | Cast (_, _, _) (* Is this expected? *)
+          | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
+            | Construct _ -> user_err Pp.(str "Match_subterm")))
   in
   try matchrec cl
   with ex when precatchable_exception ex ->
@@ -1854,7 +1861,11 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
             | Lambda (_,t,c) ->
 		bind (matchrec t) (matchrec c)
 
-            | _ -> fail "Match_subterm"))
+          | Cast (_, _, _)  -> fail "Match_subterm" (* Is this expected? *)
+
+          | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
+            | Construct _ -> fail "Match_subterm"))
+
   in
   let res = matchrec cl [] in
   match res with