Make some functions on terms more robust w.r.t new term constructs.

Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.

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