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.

12 files changed, 157 insertions, 59 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
 
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index e1b086b75..fa12e5406 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -480,7 +480,8 @@ let rec lft_fconstr n ft =
     | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
     | FLIFT(k,m) -> lft_fconstr (n+k) m
     | FLOCKED -> assert false
-    | _ -> {norm=ft.norm; term=FLIFT(n,ft)}
+    | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _
+      | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)}
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
@@ -958,7 +959,10 @@ let rec knr info m stk =
       (match evar_value info.i_cache ev with
           Some c -> knit info env c stk
         | None -> (m,stk))
-  | _ -> (m,stk)
+  | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
+    | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
+    | FCLOS _ -> (m, stk)
+
 
 (* Computes the weak head normal form of a term *)
 and kni info m stk =
@@ -1034,7 +1038,8 @@ and norm_head info m =
           mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
       | FProj (p,c) ->
           mkProj (p, kl info c)
-      | t -> term_of_fconstr m
+      | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
+        | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
 
 (* Initialization and then normalization *)
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index cec00c04b..892414e45 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -513,6 +513,7 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
   | Prod (_,t1,c1), Prod (_,t2,c2) -> eq t1 t2 && leq c1 c2
   | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq t1 t2 && eq c1 c2
   | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq b1 b2 && eq t1 t2 && leq c1 c2
+  (* Why do we suddenly make a special case for Cast here? *)
   | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2
   | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2))
   | App (c1,l1), App (c2,l2) ->
@@ -530,7 +531,9 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
       && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
       Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
-  | _ -> false
+  | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _
+     | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
+     | CoFix _), _ -> false
 
 (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
    the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
@@ -650,9 +653,6 @@ let always_true _ _ = true
 let rec eq_constr_nounivs m n =
   (m == n) || compare_head_gen (fun _ -> always_true) always_true eq_constr_nounivs m n
 
-(** We only use this function over blocks! *)
-let tag t = Obj.tag (Obj.repr t)
-
 let constr_ord_int f t1 t2 =
   let (=?) f g i1 i2 j1 j2=
     let c = f i1 i2 in
@@ -664,35 +664,50 @@ let constr_ord_int f t1 t2 =
     ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2
   in
   match kind t1, kind t2 with
+    | Cast (c1,_,_), _ -> f c1 t2
+    | _, Cast (c2,_,_) -> f t1 c2
+    (* Why this special case? *)
+    | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
+    | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
     | Rel n1, Rel n2 -> Int.compare n1 n2
-    | Meta m1, Meta m2 -> Int.compare m1 m2
+    | Rel _, _ -> -1 | _, Rel _ -> 1
     | Var id1, Var id2 -> Id.compare id1 id2
+    | Var _, _ -> -1 | _, Var _ -> 1
+    | Meta m1, Meta m2 -> Int.compare m1 m2
+    | Meta _, _ -> -1 | _, Meta _ -> 1
+    | Evar (e1,l1), Evar (e2,l2) ->
+        (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
+    | Evar _, _ -> -1 | _, Evar _ -> 1
     | Sort s1, Sort s2 -> Sorts.compare s1 s2
-    | Cast (c1,_,_), _ -> f c1 t2
-    | _, Cast (c2,_,_) -> f t1 c2
+    | Sort _, _ -> -1 | _, Sort _ -> 1
     | Prod (_,t1,c1), Prod (_,t2,c2)
     | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
         (f =? f) t1 t2 c1 c2
+    | Prod _, _ -> -1 | _, Prod _ -> 1
+    | Lambda _, _ -> -1 | _, Lambda _ -> 1
     | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
         ((f =? f) ==? f) b1 b2 t1 t2 c1 c2
-    | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
-    | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
+    | LetIn _, _ -> -1 | _, LetIn _ -> 1
     | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
-    | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
-    | Evar (e1,l1), Evar (e2,l2) ->
-        (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
+    | App _, _ -> -1 | _, App _ -> 1
     | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2
+    | Const _, _ -> -1 | _, Const _ -> 1
     | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2
+    | Ind _, _ -> -1 | _, Ind _ -> 1
     | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2
+    | Construct _, _ -> -1 | _, Construct _ -> 1
     | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
         ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
+    | Case _, _ -> -1 | _, Case _ -> 1
     | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
         ((fix_cmp =? (Array.compare f)) ==? (Array.compare f))
         ln1 ln2 tl1 tl2 bl1 bl2
+    | Fix _, _ -> -1 | _, Fix _ -> 1
     | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
         ((Int.compare =? (Array.compare f)) ==? (Array.compare f))
         ln1 ln2 tl1 tl2 bl1 bl2
-    | t1, t2 -> Int.compare (tag t1) (tag t2)
+    | CoFix _, _ -> -1 | _, CoFix _ -> 1
+    | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
 
 let rec compare m n=
   constr_ord_int compare m n
@@ -776,7 +791,9 @@ let hasheq t1 t2 =
       && array_eqeq lna1 lna2
       && array_eqeq tl1 tl2
       && array_eqeq bl1 bl2
-    | _ -> false
+    | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _
+      | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _
+      | Fix _ | CoFix _), _ -> false
 
 (** Note that the following Make has the side effect of creating
     once and for all the table we'll use for hash-consing all constr *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cb03a4d6b..aad12207e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -809,8 +809,11 @@ let rec subterm_specif renv stack t =
 	| Dead_code -> Dead_code
 	| Not_subterm -> Not_subterm)
 
+    | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
+      | Construct _ | CoFix _ -> Not_subterm
+
+
       (* Other terms are not subterms *)
-    | _ -> Not_subterm
 
 and lazy_subterm_specif renv stack t =
   lazy (subterm_specif renv stack t)
@@ -1193,8 +1196,8 @@ let check_one_cofix env nbfix def deftype =
 	| Meta _ -> ()
         | Evar _ ->
 	    List.iter (check_rec_call env alreadygrd n tree vlra) args
-
-	| _    -> raise (CoFixGuardError (env,NotGuardedForm t)) in
+        | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _
+          | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
 
   let ((mind, _),_) = codomain_is_coind env deftype in
   let vlra = lookup_subterms env mind in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index bf998933e..41d6c05eb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -57,7 +57,9 @@ let compare_stack_shape stk1 stk2 =
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
-    | (_,_) -> false in
+    | [], _ :: _
+    | (Zproj _ | ZcaseT _ | Zfix _) :: _, _ -> false
+  in
   compare_rec 0 stk1 stk2
 
 type lft_constr_stack_elt =
@@ -122,14 +124,17 @@ let nf_betaiota env t =
 
 let whd_betaiotazeta env x =
   match kind x with
-    | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
+  | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> x
     | App (c, _) ->
       begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
-      | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+      | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
+        | Case _ | Fix _ | CoFix _ | Proj _ ->
+         whd_val (create_clos_infos betaiotazeta env) (inject x)
       end
-    | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+    | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ ->
+        whd_val (create_clos_infos betaiotazeta env) (inject x)
 
 let whd_all env t =
   match kind t with
@@ -138,9 +143,12 @@ let whd_all env t =
     | App (c, _) ->
       begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ -> t
-      | _ -> whd_val (create_clos_infos all env) (inject t)
+      | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
+        | Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
+         whd_val (create_clos_infos all env) (inject t)
       end
-    | _ -> whd_val (create_clos_infos all env) (inject t)
+    | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ ->
+        whd_val (create_clos_infos all env) (inject t)
 
 let whd_allnolet env t =
   match kind t with
@@ -149,9 +157,12 @@ let whd_allnolet env t =
     | App (c, _) ->
       begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
-      | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+      | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
+        | Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
+         whd_val (create_clos_infos allnolet env) (inject t)
       end
-    | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+    | Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ ->
+        whd_val (create_clos_infos allnolet env) (inject t)
 
 (********************************************************************)
 (*                         Conversion                               *)
@@ -578,10 +589,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
      | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
        | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
-       | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
+       | (FLOCKED,_) | (_,FLOCKED) ) | (FCast _, _) | (_, FCast _) -> assert false
 
-     (* In all other cases, terms are not convertible *)
-     | _ -> raise NotConvertible
+     | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
+        | FProd _ | FEvar _), _ -> raise NotConvertible
 
 and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 47e812319..4ae875cd7 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -302,7 +302,7 @@ let rec extract_type env db j c args =
        if Projection.unfolded p then Tunknown
        else extract_type env db j (mkProj (Projection.unfold p, t)) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
-    | _ -> assert false
+    | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false
 
 (*s Auxiliary function dealing with type application.
   Precondition: [r] is a type scheme represented by the signature [s],
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
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 6c8130d79..901f366ec 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -95,13 +95,20 @@ struct
 
   let compare cmp t1 t2 = match t1, t2 with
   | DRel, DRel -> 0
+  | DRel, _ -> -1 | _, DRel -> 1
   | DSort, DSort -> 0
+  | DSort, _ -> -1 | _, DSort -> 1
   | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
+  | DRef _, _ -> -1 | _, DRef _ -> 1
+
   | DCtx (tl1, tr1), DCtx (tl2, tr2)
   | DLambda (tl1, tr1), DLambda (tl2, tr2)
   | DApp (tl1, tr1), DApp (tl2, tr2) ->
     let c = cmp tl1 tl2 in
     if c = 0 then cmp tr1 tr2 else c
+  | DCtx _, _ -> -1 | _, DCtx _ -> 1
+  | DLambda _, _ -> -1 | _, DLambda _ -> 1
+  | DApp _, _ -> -1 | _, DApp _ -> 1
 
   | DCase (ci1, c1, t1, p1), DCase (ci2, c2, t2, p2) ->
     let c = cmp c1 c2 in
@@ -113,6 +120,7 @@ struct
         else c
       else c
     else c
+  | DCase _, _ -> -1 | _, DCase _ -> 1
 
   | DFix (i1, j1, tl1, pl1), DFix (i2, j2, tl2, pl2) ->
     let c = Int.compare j1 j2 in
@@ -124,6 +132,8 @@ struct
         else c
       else c
     else c
+  | DFix _, _ -> -1 | _, DFix _ -> 1
+
   | DCoFix (i1, tl1, pl1), DCoFix (i2, tl2, pl2) ->
     let c = Int.compare i1 i2 in
     if c = 0 then
@@ -131,7 +141,18 @@ struct
       if c = 0 then Array.compare cmp pl1 pl2
       else c
     else c
-  | _ -> Pervasives.compare t1 t2 (** OK **)
+  | DCoFix _, _ -> -1 | _, DCoFix _ -> 1
+
+  | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) ->
+     let c = cmp t1 t2 in
+     if Int.equal c 0 then
+       let c = Option.compare cmp ot1 ot2 in
+       if Int.equal c 0 then cmp u1 u2
+       else c
+     else c
+  | DCons _, _ -> -1 | _, DCons _ -> 1
+
+  | DNil, DNil -> 0
 
   let fold f acc = function
     | (DRel | DNil | DSort | DRef _) -> acc
@@ -174,7 +195,8 @@ struct
 	    Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
 	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
 	    f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
-	| _ -> assert false
+        | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
+           | DFix _ | DCoFix _ | DCons _), _ -> assert false
 
   let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t =
     let head w = map (fun _ -> ()) w in
@@ -194,7 +216,8 @@ struct
 	    DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
 	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
 	    DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
-	| _ -> assert false
+        | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
+           | DFix _ | DCoFix _ | DCons _), _ -> assert false
 
   let terminal = function
     | (DRel | DSort | DNil | DRef _) -> true