GROS COMMIT:

 - reduction du noyau (variables existentielles, fonctions auxiliaires
   pour inventer des noms, etc. deplacees hors de kernel/)
 - changement de noms de constructeurs des constr (suppression de "Is" et
   "Mut")


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 365 insertions, 356 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6bd773698b..a1b251c7af 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -11,7 +11,9 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
+open Termops
 open Sign
 open Inductive
 open Evd
@@ -32,6 +34,8 @@ open Libobject
 open Library
 open Vernacinterp
 open Printer
+open Nametab
+open Declarations
 
 (****************************************************************************)
 (*            The Type of Constructions Autotactic Hints                    *)
@@ -186,7 +190,7 @@ let (inAutoHint,outAutoHint) =
 (**************************************************************************)
 
 let rec nb_hyp c = match kind_of_term c with
-  | IsProd(_,_,c2) -> if dependent (mkRel 1) c2 then nb_hyp c2 else 1+(nb_hyp c2)
+  | Prod(_,_,c2) -> if dependent (mkRel 1) c2 then nb_hyp c2 else 1+(nb_hyp c2)
   | _ -> 0 
 
 (* adding and removing tactics in the search table *)
@@ -198,7 +202,7 @@ let try_head_pattern c =
 let make_exact_entry name (c,cty) =
   let cty = strip_outer_cast cty in
   match kind_of_term cty with
-    | IsProd (_,_,_) -> 
+    | Prod (_,_,_) -> 
 	failwith "make_exact_entry"
     | _ ->
 	(head_of_constr_reference (List.hd (head_constr cty)),
@@ -207,7 +211,7 @@ let make_exact_entry name (c,cty) =
 let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
   let cty = hnf_constr env sigma cty in
   match kind_of_term cty with
-    | IsProd _ ->
+    | Prod _ ->
         let ce = mk_clenv_from () (c,cty) in
 	let c' = (clenv_template_type ce).rebus in
 	let pat = Pattern.pattern_of_constr c' in
@@ -374,14 +378,16 @@ let _ =
 	   begin 
 	     try
 	       let env = Global.env() and sigma = Evd.empty in
-	       let isp = destMutInd (Declare.global_qualified_reference qid) in
+	       let isp = destInd (Declare.global_qualified_reference qid) in
 	       let conspaths =
-		 mis_conspaths (Global.lookup_mind_specif isp) in
+                 let (mib,mip) = Global.lookup_inductive isp in
+                 mip.mind_consnames in
 	       let lcons = 
 		 array_map_to_list
-		   (fun sp ->
-		      let c = Declare.global_absolute_reference sp in
-		      (basename sp, c))
+		   (fun id ->
+                     let sp = make_path (dirpath (fst isp)) id in
+		     let c = Declare.global_absolute_reference sp in
+		      (id, c))
 		   conspaths in
 	       let dbnames = if l = [] then ["core"] else 
 	      	 List.map (function VARG_IDENTIFIER i -> string_of_id i
@@ -726,7 +732,7 @@ let decomp_unary_term c gls =
 
 let decomp_empty_term c gls = 
   let typc = pf_type_of gls c in 
-  let (hd,_) = decomp_app typc in 
+  let (hd,_) = decompose_app typc in 
   if Hipattern.is_empty_type hd then 
     simplest_case c gls 
   else 
@@ -874,7 +880,8 @@ let compileAutoArg contac = function
 	 tclFIRST 
            (List.map 
               (fun (id,_,typ) -> 
-                 if (Hipattern.is_conjunction (hd_of_prod (body_of_type typ)))
+                let cl = snd (decompose_prod (body_of_type typ)) in
+                 if (Hipattern.is_conjunction cl)
 		 then 
 		   (tclTHEN
                       (tclTHEN (simplest_elim (mkVar id)) 
@@ -918,7 +925,7 @@ let rec super_search n db_list local_db argl goal =
 let search_superauto n to_add argl g = 
   let sigma =
     List.fold_right
-      (fun (id,c) -> add_named_assum (id, pf_type_of g c))
+      (fun (id,c) -> add_named_decl (id, None, pf_type_of g c))
       to_add empty_named_context in
   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
   let db = Hint_db.add_list db0 (make_local_hint_db g) in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index bff61a8497..504cb8ba93 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -19,6 +19,7 @@ open Clenv
 open Pattern
 open Environ
 open Evd
+open Nametab
 (*i*)
   
 type auto_tactic = 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 24beccf3b7..3928d6a5ed 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -12,6 +12,7 @@ open Pp
 open Util
 open Names
 open Term
+open Termops
 open Sign
 open Reduction
 open Proof_type
@@ -79,9 +80,10 @@ let prolog_tac l n gl =
     errorlabstrm "Prolog.prolog" [< 'sTR "Prolog failed" >]
 
 let evars_of evc c = 
-  let rec evrec acc c = match splay_constr c with
-    | OpEvar n, _ when Evd.in_dom evc n -> c :: acc
-    | _, cl -> Array.fold_left evrec acc cl
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) when Evd.in_dom evc n -> c :: acc
+    | _ -> fold_constr evrec acc c
   in 
   evrec [] c
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index fed7568149..a79186719d 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -12,9 +12,10 @@ open Pp
 open Util
 open Names
 open Term
+open Termops
 open Environ
 open Reduction
-open Inductive
+open Inductiveops
 open Proof_type
 open Clenv
 open Hipattern
@@ -104,7 +105,7 @@ let inductive_of_qualid gls qid =
     with Not_found -> Nametab.error_global_not_found qid
   in
   match kind_of_term c with
-    | IsMutInd ity -> ity
+    | Ind ity -> ity
     | _ ->
 	errorlabstrm "Decompose"
 	  [< Nametab.pr_qualid qid; 'sTR " is not an inductive type" >]
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index ae2d8a4a59..d2d2dadd5e 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -10,7 +10,9 @@
 
 open Util
 open Names
+open Nameops
 open Term
+open Declarations
 open Tactics
 open Tacticals
 open Hiddentac
@@ -65,9 +67,9 @@ let h_solveRightBranch =
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
 let mkDecideEqGoal rectype c1 c2 g = 
-  let equality    = mkAppA [|build_coq_eq_data.eq (); rectype; c1; c2|] in
-  let disequality = mkAppA [|build_coq_not (); equality|] in
-  mkAppA [|build_coq_sumbool (); equality; disequality |]
+  let equality    = mkApp(build_coq_eq_data.eq (), [|rectype; c1; c2|]) in
+  let disequality = mkApp(build_coq_not (), [|equality|]) in
+  mkApp(build_coq_sumbool (), [|equality; disequality |])
 
 
 (* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
@@ -110,8 +112,9 @@ let solveLeftBranch rectype g =
     with Pattern.PatternMatchingFailure -> error "Unexpected conclusion!"
   with 
     | _ :: lhs :: rhs :: _ -> 
-	let nparams   = Global.mind_nparams rectype in
-	let getargs l = snd (list_chop nparams (snd (decomp_app l))) in
+        let (mib,mip) = Global.lookup_inductive rectype in
+	let nparams   = mip.mind_nparams in
+	let getargs l = snd (list_chop nparams (snd (decompose_app l))) in
 	let rargs   = getargs (snd rhs)
 	and largs   = getargs (snd lhs) in 
 	List.fold_right2 
@@ -122,7 +125,7 @@ let solveLeftBranch rectype g =
 (* The tactic Decide Equality *)
 
 let hd_app c = match kind_of_term c with
-  | IsApp (h,_) -> h
+  | App (h,_) -> h
   | _ -> c
 
 let decideGralEquality g =
@@ -135,7 +138,7 @@ let decideGralEquality g =
 	let headtyp = hd_app (pf_compute g typ) in
 	let rectype =
 	  match kind_of_term headtyp with
-            | IsMutInd mi -> mi
+            | Ind mi -> mi
 	    | _ -> error 
 		"This decision procedure only works for inductive objects" 
 	in 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2137b4f1c9..d1ac66b1fc 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -13,9 +13,11 @@ open Util
 open Names
 open Univ
 open Term
+open Termops
 open Inductive
+open Inductiveops
 open Environ
-open Reduction
+open Reductionops
 open Instantiate
 open Typeops
 open Typing
@@ -34,6 +36,7 @@ open Tacred
 open Vernacinterp
 open Coqlib
 open Setoid_replace
+open Declarations
 
 (* Rewriting tactics *)
 
@@ -57,7 +60,7 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
 	else error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
         let hdcncls = string_of_inductive hdcncl in 
-	let suffix = Declare.elimination_suffix (elimination_sort_of_goal gl)in
+	let suffix = Indrec.elimination_suffix (elimination_sort_of_goal gl)in
         let elim =
 	  if lft2rgt then
             pf_global gl (id_of_string (hdcncls^suffix^"_r"))
@@ -105,8 +108,8 @@ let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl =
   if unsafe or (pf_conv_x gl t1 t2) then
     let (e,sym) = 
       match kind_of_term (hnf_type_of gl t1) with 
-        | IsSort (Prop(Pos)) -> (eq,sym_eq)
-        | IsSort (Type(_))   -> (eqt,sym_eqt)
+        | Sort (Prop(Pos)) -> (eq,sym_eq)
+        | Sort (Type(_))   -> (eqt,sym_eqt)
         | _                  -> error "replace"
     in 
     (tclTHENL (elim_type (applist (e, [t1;c1;c2])))
@@ -176,7 +179,7 @@ let v_conditional_rewriteRL =
 let find_constructor env sigma c =
   let hd,stack = whd_betadeltaiota_stack env sigma c in
   match kind_of_term hd with
-    | IsMutConstruct _ -> (hd,stack)
+    | Construct _ -> (hd,stack)
     | _ -> error "find_constructor"
 
 (* Patterns *)
@@ -204,23 +207,24 @@ type elimination_types =
 
 let necessary_elimination sort_arity sort =
   let sort_arity = mkSort sort_arity in
-  if (isType sort) then
-    if is_Set sort_arity then
-      Set_Type
-    else 
-      if is_Type sort_arity then
-	Type_Type
-      else  
-	errorlabstrm "necessary_elimination" 
-	  [< 'sTR "no primitive equality on proofs" >]  
-  else
-    if is_Set sort_arity then
-      Set_SetorProp
-    else
-      if is_Type sort_arity then
-	Type_SetorProp
-      else  errorlabstrm "necessary_elimination" 
-        [< 'sTR "no primitive equality on proofs" >]
+  match sort with
+      Type _ ->
+        if is_Set sort_arity then
+          Set_Type
+        else 
+          if is_Type sort_arity then
+	    Type_Type
+          else  
+	    errorlabstrm "necessary_elimination" 
+	      [< 'sTR "no primitive equality on proofs" >]  
+    | _ ->
+        if is_Set sort_arity then
+          Set_SetorProp
+        else
+          if is_Type sort_arity then
+	    Type_SetorProp
+          else  errorlabstrm "necessary_elimination" 
+            [< 'sTR "no primitive equality on proofs" >]
 
 let find_eq_pattern aritysort sort = 
   match necessary_elimination aritysort sort with
@@ -273,7 +277,7 @@ let find_positions env sigma t1 t2 =
     let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in
     match (kind_of_term hd1, kind_of_term hd2) with
   	
-      | IsMutConstruct sp1, IsMutConstruct sp2 ->
+      | Construct sp1, Construct sp2 ->
         (* both sides are constructors, so either we descend, or we can
            discriminate here. *)
 	  if sp1 = sp2 then
@@ -378,21 +382,24 @@ let descend_then sigma env head dirn =
   let IndType (indf,_) as indt =
     try find_rectype env sigma (get_type_of env sigma head)
     with Not_found -> assert false in
-  let mispec,_ = dest_ind_family indf in
-  let cstr = get_constructors indf in
+  let ind,_ = dest_ind_family indf in
+  let (mib,mip) = lookup_mind_specif env ind in
+  let cstr = get_constructors env indf in
   let dirn_nlams = cstr.(dirn-1).cs_nargs in
   let dirn_env = push_rels cstr.(dirn-1).cs_args env in
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let arign,_ = get_arity indf in
-      let p = it_mkLambda_or_LetIn (lift (mis_nrealargs mispec) resty) arign in
+      let arign,_ = get_arity env indf in
+      let p = it_mkLambda_or_LetIn (lift mip.mind_nrealargs resty) arign in
       let build_branch i =
 	let result = if i = dirn then dirnval else dfltval in
-	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args
-      in
-      mkMutCaseL (make_default_case_info mispec, p, head,
-		 List.map build_branch (interval 1 (mis_nconstr mispec)))))
+	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
+      let brl =
+        List.map build_branch
+          (interval 1 (Array.length mip.mind_consnames)) in
+      let ci = make_default_case_info env ind in
+      mkCase (ci, p, head, Array.of_list brl)))
   
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -412,7 +419,7 @@ let descend_then sigma env head dirn =
    giving [True], and all the rest giving False. *)
 
 let construct_discriminator sigma env dirn c sort =
-  let (IndType(IndFamily (mispec,_) as indf,_) as indt) =
+  let (IndType((ind,_) as indf,_) as indt) =
     try find_rectype env sigma (type_of env sigma c)
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors 
@@ -423,7 +430,8 @@ let construct_discriminator sigma env dirn c sort =
       errorlabstrm "Equality.construct_discriminator"
 	[< 'sTR "Cannot discriminate on inductive constructors with 
 		 dependent types" >] in
-  let arsign,arsort = get_arity indf in
+  let (mib,mip) = lookup_mind_specif env ind in
+  let arsign,arsort = get_arity env indf in
   let (true_0,false_0,sort_0) = 
     match necessary_elimination arsort (destSort sort) with
       | Type_Type ->
@@ -431,25 +439,24 @@ let construct_discriminator sigma env dirn c sort =
       | _         -> build_coq_True (),  build_coq_False (), (Prop Null)
   in
   let p = it_mkLambda_or_LetIn (mkSort sort_0) arsign in
-  let cstrs = get_constructors indf in
+  let cstrs = get_constructors env indf in
   let build_branch i =
     let endpt = if i = dirn then true_0 else false_0 in
-    it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args 
-  in
-  let build_match =
-    mkMutCaseL (make_default_case_info mispec, p, c,
-	       List.map build_branch (interval 1 (mis_nconstr mispec)))
-  in
-  build_match
+    it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in
+  let brl =
+    List.map build_branch(interval 1 (Array.length mip.mind_consnames)) in
+  let ci = make_default_case_info env ind in
+  mkCase (ci, p, c, Array.of_list brl)
     
 let rec build_discriminator sigma env dirn c sort = function
   | [] -> construct_discriminator sigma env dirn c sort
   | ((sp,cnum),argnum)::l ->
       let cty = type_of env sigma c in
-      let IndType (indf,_) =
+      let IndType ((ind,_)as indf,_) =
 	try find_rectype env sigma cty with Not_found -> assert false in
-      let _,arsort = get_arity indf in
-      let nparams = mis_nparams (fst (dest_ind_family indf)) in
+      let (mib,mip) = lookup_mind_specif env ind in
+      let _,arsort = get_arity env indf in
+      let nparams = mip.mind_nparams  in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
       let newc = mkRel(cnum_nlams-(argnum-nparams)) in
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
@@ -489,7 +496,8 @@ let gen_absurdity id gl =
 let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
   let env = pf_env gls in
   let (indt,_) = find_mrectype env (project gls) t in 
-  let aritysort = mis_sort (Global.lookup_mind_specif indt) in
+  let (mib,mip) = lookup_mind_specif env indt in
+  let aritysort = mip.mind_sort in
   let sort = pf_type_of gls (pf_concl gls) in
   match necessary_elimination aritysort (destSort sort) with
     | Type_Type  ->
@@ -530,7 +538,7 @@ let discr id gls =
 	 errorlabstrm "discr" [< 'sTR" Not a discriminable equality" >]
      | Inl (cpath, (_,dirn), _) ->
 	 let e = pf_get_new_id (id_of_string "ee") gls in
-	 let e_env = push_named_assum (e,t) env in
+	 let e_env = push_named_decl (e,None,t) env in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (indt,_) = find_mrectype env sigma t in 
@@ -601,7 +609,7 @@ let make_tuple env sigma (prev_lind,rterm,rty) lind =
   let {intro = exist_term; typ = sig_term} =
     find_sigma_data (get_sort_of env sigma rty) in
   let a = type_of env sigma (mkRel lind) in
-  let na = fst (lookup_rel_type lind env) in
+  let (na,_,_) = lookup_rel lind env in
   (* If [lind] is not [prev_lind+1] then we lift down rty *)
   let rty = lift (- lind + prev_lind + 1) rty in
   (* Now [lind] is [mkRel 1] and we abstract on (na:a) *)
@@ -729,7 +737,8 @@ let rec build_injrec sigma env (t1,t2) c = function
   | ((sp,cnum),argnum)::l ->
       let cty = type_of env sigma c in
       let (ity,_) = find_mrectype env sigma cty in
-      let nparams = Global.mind_nparams ity in
+      let (mib,mip) = lookup_mind_specif env ity in
+      let nparams = mip.mind_nparams in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
       let newc = mkRel(cnum_nlams-(argnum-nparams)) in
       let (subval,tuplety,dfltval) =
@@ -746,9 +755,9 @@ let try_delta_expand env sigma t =
   let whdt = whd_betadeltaiota env sigma t  in 
   let rec hd_rec c  =
     match kind_of_term c with
-      | IsMutConstruct _ -> whdt
-      | IsApp (f,_)  -> hd_rec f
-      | IsCast (c,_) -> hd_rec c
+      | Construct _ -> whdt
+      | App (f,_)  -> hd_rec f
+      | Cast (c,_) -> hd_rec c
       | _  -> t
   in 
   hd_rec whdt 
@@ -778,7 +787,7 @@ let inj id gls =
 	   [<'sTR"Nothing to do, it is an equality between convertible terms">]
     | Inr posns ->
 	let e = pf_get_new_id (id_of_string "e") gls in
-	let e_env = push_named_assum (e,t) env in
+	let e_env = push_named_decl (e,None,t) env in
 	let injectors =
 	  map_succeed
 	    (fun (cpath,t1_0,t2_0) ->
@@ -832,7 +841,7 @@ let decompEqThen ntac id gls =
   (match find_positions env sigma t1 t2 with
      | Inl (cpath, (_,dirn), _) ->
 	 let e = pf_get_new_id (id_of_string "e") gls in
-	 let e_env = push_named_assum (e,t) env in
+	 let e_env = push_named_decl (e,None,t) env in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (pf, absurd_term) =
@@ -846,7 +855,7 @@ let decompEqThen ntac id gls =
 	   [<'sTR"Nothing to do, it is an equality between convertible terms">]
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
-	  let e_env = push_named_assum (e,t) env in
+	  let e_env = push_named_decl (e,None,t) env in
 	  let injectors =
 	    map_succeed
 	      (fun (cpath,t1_0,t2_0) ->
@@ -924,8 +933,8 @@ let swapEquandsInHyp id gls =
 
 let find_elim  sort_of_gl  lbeq =
   match kind_of_term sort_of_gl  with
-    | IsSort(Prop Null)  (* Prop *)  ->  (lbeq.ind (), false)  
-    | IsSort(Prop Pos)   (* Set *)   ->  
+    | Sort(Prop Null)  (* Prop *)  ->  (lbeq.ind (), false)  
+    | Sort(Prop Pos)   (* Set *)   ->  
 	(match lbeq.rrec with
            | Some eq_rec -> (eq_rec (), false) 
 	   | None -> errorlabstrm "find_elim"
@@ -1097,54 +1106,25 @@ let rec list_int n cmr l =
 
 (* Tells if two constrs are equal modulo unification *)
 
-(* Alpha-conversion *)
-let bind_eq = function
-  | (Anonymous,Anonymous) -> true
-  | (Name _,Name _) -> true
-  | _ -> false
-
-(* TODO: Fix and CoFix also contain bound names *)
-let eqop_mod_names = function
-  | OpLambda n0, OpLambda n1 -> bind_eq (n0,n1)
-  | OpProd n0, OpProd n1 -> bind_eq (n0,n1)
-  | OpLetIn n0, OpLetIn n1 -> bind_eq (n0,n1)
-  | op0, op1 -> op0 = op1
-
 exception NotEqModRel
 
-let rec eq_mod_rel l_meta t0 t1 =
-  match splay_constr_with_binders t1 with
-    | OpMeta n, [], [||] ->
-	if not (List.mem_assoc n l_meta) then
-	  [(n,t0)]@l_meta
-	else if (List.assoc n l_meta) = t0 then
-	  l_meta
-	else
-	  raise NotEqModRel
-    | op1, bd1, v1 ->
-	match splay_constr_with_binders t0 with
-	  | op0, bd0, v0
-	      when (eqop_mod_names (op0, op1)
-		    & (List.length bd0 = List.length bd1)
-		    & (Array.length v0 = Array.length v1)) ->
-	      array_fold_left2 eq_mod_rel
-		(List.fold_left2 eq_mod_rel_binders l_meta bd0 bd1)
-		v0 v1
-	    | _ -> raise NotEqModRel
-
-  and eq_mod_rel_binders l_meta t0 t1 = match (t0,t1) with
-    | (na0,Some b0,t0), (na1,Some b1,t1) when bind_eq (na0,na1) ->
-	eq_mod_rel (eq_mod_rel l_meta b0 b1) t0 t1
-    | (na0,None,t0), (na1,None,t1) when bind_eq (na0,na1) ->
-	eq_mod_rel l_meta t0 t1
-    | _ -> raise NotEqModRel
+let eq_mod_rel l_meta t0 t1 =
+  let bindings = ref l_meta in
+  let rec eq_rec t0 t1 = 
+    match kind_of_term t1 with
+      | Meta n ->
+	  if not (List.mem_assoc n !bindings) then
+	    (bindings := (n,t0) :: !bindings; true)
+	  else (List.assoc n l_meta) = t0
+      | _ -> compare_constr eq_rec t0 t1 in
+  if eq_rec t0 t1 then !bindings else raise NotEqModRel
 
 (* Verifies if the constr has an head constant *)
 
 let is_hd_const c = match kind_of_term c with
-  | IsApp (f,args) ->
+  | App (f,args) ->
       (match kind_of_term f with
-         | IsConst c -> Some (c, args)
+         | Const c -> Some (c, args)
          |_ -> None)
   | _ -> None
 
@@ -1154,10 +1134,10 @@ let is_hd_const c = match kind_of_term c with
 
 let nb_occ_term t u =
   let rec nbrec nocc u =
-    if t = u then   (* Pourquoi pas eq_constr ?? *)
+    if eq_constr t u then
       nocc + 1
     else
-      Array.fold_left nbrec nocc (snd (splay_constr u))
+      fold_constr nbrec nocc u
   in nbrec 0 u
     
 
@@ -1166,35 +1146,24 @@ let nb_occ_term t u =
    Rem: t_eq is assumed closed then there is no need to lift it
 *)
 let sub_term_with_unif cref ceq =
-  let rec find_match l_meta nb_occ hdsp t_args u = match splay_constr u with
-    | OpApp, cl -> begin
-	let f, args = destApplication u in
-	match kind_of_term f with
-          | IsConst sp when sp = hdsp -> begin
+  let rec find_match hdsp t_args (l_meta,nb_occ) u =
+    match kind_of_term u with
+    | App(f,args) ->
+	(match kind_of_term f with
+          | Const sp when sp = hdsp -> begin
 	      try (array_fold_left2 eq_mod_rel l_meta args t_args, nb_occ+1)
 	      with NotEqModRel ->
-		Array.fold_left
-                  (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ
-                       hdsp t_args x) (l_meta,nb_occ) args
+		Array.fold_left (find_match hdsp t_args) (l_meta,nb_occ) args
 	    end
 
-          | IsConst _ | IsVar _ | IsMutInd _ | IsMutConstruct _
-	  | IsFix _ | IsCoFix _ ->
-               Array.fold_left 
-		 (fun (l_meta,nb_occ) x -> find_match l_meta
-		      nb_occ hdsp t_args x) (l_meta,nb_occ) cl
+          | (Const _ | Var _ | Ind _ | Construct _ | Fix _ | CoFix _) ->
+              fold_constr (find_match hdsp t_args) (l_meta,nb_occ) u
 
 	   (* Pourquoi ne récurre-t-on pas dans f ? *)
-           | _ -> (l_meta,nb_occ)
-      end
+           | _ -> (l_meta,nb_occ))
 
-(* Le code original ne récurrait pas sous les Cast 
-    | OpCast, _ -> (l_meta,nb_occ)
-*)
-    | _, t -> 
-	Array.fold_left 
-	  (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ hdsp t_args x)
-	  (l_meta,nb_occ) t
+    | _ ->
+        fold_constr (find_match hdsp t_args) (l_meta,nb_occ) u
 
   in
   match (is_hd_const ceq) with
@@ -1208,7 +1177,7 @@ let sub_term_with_unif cref ceq =
           else
             Some (ceq,nb_occ)
     |Some (head,t_args) ->
-        let (l,nb) = find_match [] 0 head t_args cref in
+        let (l,nb) = find_match head t_args ([],0) cref in
         if nb = 0 then
           None
         else
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index a3bdf52b99..e6def959b5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -11,15 +11,18 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
-open Reduction
-open Inductive
+open Termops
+open Reductionops
+open Inductiveops
 open Evd
 open Environ
 open Proof_trees
 open Clenv
 open Pattern
 open Coqlib
+open Declarations
 
 (* I implemented the following functions which test whether a term t
    is an inductive but non-recursive type, a general conjuction, a
@@ -39,11 +42,11 @@ let op2bool = function Some _ -> true | None -> false
 
 let match_with_non_recursive_type t = 
   match kind_of_term t with 
-    | IsApp _ -> 
-        let (hdapp,args) = decomp_app t in
+    | App _ -> 
+        let (hdapp,args) = decompose_app t in
         (match kind_of_term hdapp with
-           | IsMutInd ind -> 
-               if not (Global.mind_is_recursive ind) then 
+           | Ind ind -> 
+               if not (Global.lookup_mind (fst ind)).mind_finite then 
 		 Some (hdapp,args) 
 	       else 
 		 None 
@@ -56,12 +59,13 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
    only one constructor. *)
 
 let match_with_conjunction t =
-  let (hdapp,args) = decomp_app t in 
+  let (hdapp,args) = decompose_app t in 
   match kind_of_term hdapp with
-    | IsMutInd ind -> 
-	let mispec = Global.lookup_mind_specif ind in
-	if (mis_nconstr mispec = 1)
-	  && (not (mis_is_recursive mispec)) && (mis_nrealargs mispec = 0)
+    | Ind ind -> 
+	let (mib,mip) = Global.lookup_inductive ind in
+	if (Array.length mip.mind_consnames = 1)
+	  && (not (mis_is_recursive (mib,mip)))
+          && (mip.mind_nrealargs = 0)
         then 
 	  Some (hdapp,args)
         else 
@@ -74,15 +78,15 @@ let is_conjunction t = op2bool (match_with_conjunction t)
    whose constructors have a single argument. *)
 
 let match_with_disjunction t =
-  let (hdapp,args) = decomp_app t in 
+  let (hdapp,args) = decompose_app t in 
   match kind_of_term hdapp with
-    | IsMutInd ind  ->
-	let mispec = Global.lookup_mind_specif ind in
-        let constr_types = mis_nf_lc mispec in
+    | Ind ind  ->
+	let (mib,mip) = Global.lookup_inductive ind in
+        let constr_types = mip.mind_nf_lc in
         let only_one_arg c =
-	  ((nb_prod c) - (mis_nparams mispec)) = 1 in 
+	  ((nb_prod c) - mip.mind_nparams) = 1 in 
 	if (array_for_all only_one_arg constr_types) &&
-          (not (mis_is_recursive mispec))
+          (not (mis_is_recursive (mib,mip)))
         then 
 	  Some (hdapp,args)
         else 
@@ -92,22 +96,25 @@ let match_with_disjunction t =
 let is_disjunction t = op2bool (match_with_disjunction t)
 
 let match_with_empty_type t =
-  let (hdapp,args) = decomp_app t in
+  let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
-    | IsMutInd ind -> 
-        let nconstr = Global.mind_nconstr ind in  
+    | Ind ind -> 
+        let (mib,mip) = Global.lookup_inductive ind in
+        let nconstr = Array.length mip.mind_consnames in  
 	if nconstr = 0 then Some hdapp else None
     | _ ->  None
 	  
 let is_empty_type t = op2bool (match_with_empty_type t)
 
 let match_with_unit_type t =
-  let (hdapp,args) = decomp_app t in
+  let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
-    | IsMutInd ind  -> 
-        let constr_types = Global.mind_nf_lc ind in 
-        let nconstr = Global.mind_nconstr ind in
-        let zero_args c =  nb_prod c = Global.mind_nparams ind in  
+    | Ind ind  -> 
+        let (mib,mip) = Global.lookup_inductive ind in
+        let constr_types = mip.mind_nf_lc in 
+        let nconstr = Array.length mip.mind_consnames in
+        let zero_args c =
+          nb_prod c = mip.mind_nparams in  
 	if nconstr = 1 && array_for_all zero_args constr_types then 
 	  Some hdapp
         else 
@@ -122,11 +129,12 @@ let is_unit_type t = op2bool (match_with_unit_type t)
    establishing its reflexivity.  *)
 
 let match_with_equation t =
-  let (hdapp,args) = decomp_app t in
+  let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
-    | IsMutInd ind -> 
-        let constr_types = Global.mind_nf_lc ind in 
-        let nconstr = Global.mind_nconstr ind in
+    | Ind ind -> 
+        let (mib,mip) = Global.lookup_inductive ind in
+        let constr_types = mip.mind_nf_lc in 
+        let nconstr = Array.length mip.mind_consnames in
 	if nconstr = 1 &&
            (is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0) ||
             is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0)) 
@@ -149,7 +157,7 @@ let match_with_nottype t =
 let is_nottype t = op2bool (match_with_nottype t)
 		     
 let is_imp_term c = match kind_of_term c with
-  | IsProd (_,_,b) -> not (dependent (mkRel 1) b)
+  | Prod (_,_,b) -> not (dependent (mkRel 1) b)
   | _              -> false
 
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 15e8ee6b32..c8da9ed1d9 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -12,12 +12,13 @@ open Pp
 open Util
 open Names
 open Term
+open Termops
 open Global
 open Sign
 open Environ
-open Inductive
+open Inductiveops
 open Printer
-open Reduction
+open Reductionops
 open Retyping
 open Tacmach
 open Proof_type
@@ -88,7 +89,7 @@ let make_inv_predicate env sigma ind id status concl =
     match status with
       | NoDep ->
 	  (* We push the arity and leave concl unchanged *)
-	  let hyps_arity,_ = get_arity indf in
+	  let hyps_arity,_ = get_arity env indf in
 	  (hyps_arity,concl)
       | Dep dflt_concl ->
 	  if not (dependent (mkVar id) concl) then
@@ -188,7 +189,7 @@ let rec dependent_hyps id idlist sign =
   let rec dep_rec =function
     | [] -> []
     | (id1::l) -> 
-	let id1ty = snd (lookup_named id1 sign) in  
+	let (_,_,id1ty) = lookup_named id1 sign in  
 	if occur_var (Global.env()) id (body_of_type id1ty)
         then id1::dep_rec l
         else dep_rec l
@@ -233,21 +234,21 @@ let projectAndApply thin id depids gls =
       let (t,t1,t2) = dest_eq gls (pf_get_hyp_typ gls id) in
       match (kind_of_term (strip_outer_cast t1),
 	     kind_of_term (strip_outer_cast t2)) with
-        | IsVar id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1
-        | _, IsVar id2 -> generalizeRewriteIntros (subst_hyp_RL id) depids id2
+        | Var id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1
+        | _, Var id2 -> generalizeRewriteIntros (subst_hyp_RL id) depids id2
         | _ -> subst_hyp_RL id
     in 
     onLastHyp orient_rule gls 
   in
   let (t,t1,t2) = dest_eq gls (pf_get_hyp_typ gls id)  in
   match (thin, kind_of_term (strip_outer_cast t1), kind_of_term (strip_outer_cast t2)) with
-    | (true, IsVar id1,  _) -> generalizeRewriteIntros
+    | (true, Var id1,  _) -> generalizeRewriteIntros
           (tclTHEN (subst_hyp_LR id) (clear_clause id)) depids id1 gls
-    | (false, IsVar id1,  _) ->
+    | (false, Var id1,  _) ->
         generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls
-    | (true, _ , IsVar id2) -> generalizeRewriteIntros
+    | (true, _ , Var id2) -> generalizeRewriteIntros
           (tclTHEN (subst_hyp_RL id) (clear_clause id)) depids id2 gls
-    | (false, _ , IsVar id2) ->
+    | (false, _ , Var id2) ->
         generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls
     | (true, _, _) ->
         let deq_trailer neqns =
@@ -323,7 +324,7 @@ let case_trailer othin neqns ba gl =
 
 let collect_meta_variables c = 
   let rec collrec acc c = match kind_of_term c with
-    | IsMeta mv -> mv::acc
+    | Meta mv -> mv::acc
     | _ -> fold_constr collrec acc c
   in 
   collrec [] c
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index f6b2ba06f2..ab0590a714 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -11,13 +11,15 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
+open Termops
 open Sign
 open Evd
 open Printer
-open Reduction
+open Reductionops
 open Declarations
-open Inductive
+open Inductiveops
 open Environ
 open Tacmach
 open Proof_trees
@@ -30,6 +32,7 @@ open Wcclausenv
 open Tacticals
 open Tactics
 open Inv
+open Safe_typing
 
 let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
 
@@ -131,14 +134,14 @@ let max_prefix_sign lid sign =
 *)
 let rec add_prods_sign env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
-    | IsProd (na,c1,b) ->
-	let id = Environ.id_of_name_using_hdchar env t na in
+    | Prod (na,c1,b) ->
+	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (Environ.push_named_assum (id,c1) env) sigma b'
-    | IsLetIn (na,c1,t1,b) ->
-	let id = Environ.id_of_name_using_hdchar env t na in
+        add_prods_sign (push_named_decl (id,None,c1) env) sigma b'
+    | LetIn (na,c1,t1,b) ->
+	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (Environ.push_named_def (id,c1,t1) env) sigma b'
+        add_prods_sign (push_named_decl (id,Some c1,t1) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates wether the inversion lemma is dependent or not.
@@ -180,7 +183,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       (pty,goal)
   in
   let npty = nf_betadeltaiota env sigma pty in
-  let extenv = push_named_assum (p,npty) env in
+  let extenv = push_named_decl (p,None,npty) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
@@ -224,7 +227,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     List.fold_left
       (fun (avoid,sign,mvb) (mv,mvty) ->
          let h = next_ident_away (id_of_string "H") avoid in
-	 (h::avoid, add_named_assum (h,mvty) sign, (mv,mkVar h)::mvb))
+	 (h::avoid, add_named_decl (h,None,mvty) sign, (mv,mkVar h)::mvb))
       (ids_of_context invEnv, ownSign, [])
       meta_types 
   in
@@ -271,7 +274,7 @@ let _ =
     (function
        | [VARG_NUMBER n; VARG_IDENTIFIER na; VARG_IDENTIFIER id] ->
 	   fun () ->
-	     inversion_lemma_from_goal n na id prop false inv_clear_tac
+	     inversion_lemma_from_goal n na id mk_Prop false inv_clear_tac
        | _ -> bad_vernac_args "MakeInversionLemmaFromHyp")
 
 let add_inversion_lemma_exn na com comsort bool tac =
@@ -299,7 +302,7 @@ let _ =
     (function
        | [VARG_NUMBER n; VARG_IDENTIFIER na; VARG_IDENTIFIER id] ->
 	   fun () ->
-	     inversion_lemma_from_goal n na id prop false half_inv_tac
+	     inversion_lemma_from_goal n na id mk_Prop false half_inv_tac
        | _ -> bad_vernac_args "MakeSemiInversionLemmaFromHyp")
 
 let _ = 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 6fdc75ae48..366611d43d 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -50,6 +50,7 @@ open Pp
 open Util
 open Names
 open Term
+open Termops
 open Tacmach
 open Sign
 open Environ
@@ -97,14 +98,14 @@ let replace_by_meta env = function
       let m = mkMeta n in
       (* quand on introduit une mv on calcule son type *)
       let ty = match kind_of_term c with
-	| IsLambda (Name id,c1,c2) when isCast c2 ->
+	| Lambda (Name id,c1,c2) when isCast c2 ->
 	    mkNamedProd id c1 (snd (destCast c2))
-	| IsLambda (Anonymous,c1,c2) when isCast c2 ->
+	| Lambda (Anonymous,c1,c2) when isCast c2 ->
 	    mkArrow c1 (snd (destCast c2))
-	| _ -> (* (IsApp _ | IsMutCase _) -> *)
+	| _ -> (* (App _ | Case _) -> *)
 	    Retyping.get_type_of_with_meta env Evd.empty mm c
 	(*
-	| IsFix ((_,j),(v,_,_)) ->
+	| Fix ((_,j),(v,_,_)) ->
 	    v.(j) (* en pleine confiance ! *)
 	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" 
         *)
@@ -131,25 +132,25 @@ let fresh env n =
 
 let rec compute_metamap env c = match kind_of_term c with
   (* le terme est directement une preuve *)
-  | (IsConst _ | IsEvar _ | IsMutInd _ | IsMutConstruct _ |
-    IsSort _ | IsVar _ | IsRel _) -> 
+  | (Const _ | Evar _ | Ind _ | Construct _ |
+    Sort _ | Var _ | Rel _) -> 
       TH (c,[],[])
   (* le terme est une mv => un but *)
-  | IsMeta n ->
+  | Meta n ->
       (* 
       Pp.warning (Printf.sprintf ("compute_metamap: MV(%d) sans type !\n") n);
       let ty = Retyping.get_type_of_with_meta env Evd.empty lmeta c in 
       *)
       TH (c,[],[None])
-  | IsCast (m,ty) when isMeta m -> 
+  | Cast (m,ty) when isMeta m -> 
       TH (c,[destMeta m,ty],[None])
 
   (* abstraction => il faut décomposer si le terme dessous n'est pas pur
    *    attention : dans ce cas il faut remplacer (Rel 1) par (Var x)
    *    où x est une variable FRAICHE *)
-  | IsLambda (name,c1,c2) ->
+  | Lambda (name,c1,c2) ->
       let v = fresh env name in
-      let env' = push_named_assum (v,c1) env in
+      let env' = push_named_decl (v,None,c1) env in
       begin match compute_metamap env' (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
@@ -159,11 +160,11 @@ let rec compute_metamap env c = match kind_of_term c with
 	    TH (mkLambda (Name v,c1,m), mm, sgp)
       end
 
-  | IsLetIn (name, c1, t1, c2) ->
+  | LetIn (name, c1, t1, c2) ->
       if occur_meta c1 then 
 	error "Refine: body of let-in cannot contain existentials";
       let v = fresh env name in
-      let env' = push_named_def (v,c1,t1) env in
+      let env' = push_named_decl (v,Some c1,t1) env in
       begin match compute_metamap env' (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
@@ -174,16 +175,18 @@ let rec compute_metamap env c = match kind_of_term c with
       end
 
   (* 4. Application *)
-  | IsApp (f,v) ->
+  | App (f,v) ->
       let a = Array.map (compute_metamap env) (Array.append [|f|] v) in
       begin
 	try
-	  let v',mm,sgp = replace_in_array env a in TH (mkAppA v',mm,sgp)
+	  let v',mm,sgp = replace_in_array env a in
+          let v'' = Array.sub v' 1 (Array.length v) in
+          TH (mkApp(v'.(0), v''),mm,sgp)
 	with NoMeta ->
 	  TH (c,[],[])
       end
 
-  | IsMutCase (ci,p,c,v) ->
+  | Case (ci,p,c,v) ->
       (* bof... *)
       let nbr = Array.length v in
       let v = Array.append [|p;c|] v in
@@ -192,13 +195,13 @@ let rec compute_metamap env c = match kind_of_term c with
 	try
 	  let v',mm,sgp = replace_in_array env a in
 	  let v'' = Array.sub v' 2 nbr in
-	  TH (mkMutCase (ci,v'.(0),v'.(1),v''),mm,sgp)
+	  TH (mkCase (ci,v'.(0),v'.(1),v''),mm,sgp)
 	with NoMeta ->
 	  TH (c,[],[])
       end
 
   (* 5. Fix. *)
-  | IsFix ((ni,i),(fi,ai,v)) ->
+  | Fix ((ni,i),(fi,ai,v)) ->
       (* TODO: use a fold *)
       let vi = Array.map (fresh env) fi in
       let fi' = Array.map (fun id -> Name id) vi in
@@ -217,19 +220,19 @@ let rec compute_metamap env c = match kind_of_term c with
       end
 	      
   (* Cast. Est-ce bien exact ? *)
-  | IsCast (c,t) -> compute_metamap env c
+  | Cast (c,t) -> compute_metamap env c
       (*let TH (c',mm,sgp) = compute_metamap sign c in
 	TH (mkCast (c',t),mm,sgp) *)
       
   (* Produit. Est-ce bien exact ? *)
-  | IsProd (_,_,_) ->
+  | Prod (_,_,_) ->
       if occur_meta c then
 	error "Refine: proof term contains metas in a product"
       else
       	TH (c,[],[])
 
   (* Cofix. *)
-  | IsCoFix (i,(fi,ai,v)) ->
+  | CoFix (i,(fi,ai,v)) ->
       let vi = Array.map (fresh env) fi in
       let fi' = Array.map (fun id -> Name id) vi in
       let env' = push_named_rec_types (fi',ai,v) env in
@@ -255,10 +258,10 @@ let rec compute_metamap env c = match kind_of_term c with
 let rec tcc_aux (TH (c,mm,sgp) as th) gl =
   match (kind_of_term c,sgp) with
     (* mv => sous-but : on ne fait rien *)
-    | IsMeta _ , _ ->
+    | Meta _ , _ ->
 	tclIDTAC gl
 
-    | IsCast (c,_), _ when isMeta c ->
+    | Cast (c,_), _ when isMeta c ->
 	tclIDTAC gl
 	  
     (* terme pur => refine *)
@@ -266,18 +269,18 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	refine c gl
 	
     (* abstraction => intro *)
-    | IsLambda (Name id,_,m), _ when isMeta (strip_outer_cast m) ->
+    | Lambda (Name id,_,m), _ when isMeta (strip_outer_cast m) ->
 	begin match sgp with
 	  | [None] -> introduction id gl
 	  | [Some th] -> tclTHEN (introduction id) (tcc_aux th) gl
 	  | _ -> assert false
 	end
 	
-    | IsLambda _, _ ->
+    | Lambda _, _ ->
 	anomaly "invalid lambda passed to function tcc_aux"
 
     (* let in *)
-    | IsLetIn (Name id,c1,t1,c2), _ when isMeta (strip_outer_cast c2) ->
+    | LetIn (Name id,c1,t1,c2), _ when isMeta (strip_outer_cast c2) ->
 	let c = pf_concl gl in
 	let newc = mkNamedLetIn id c1 t1 c in
 	tclTHEN 
@@ -288,11 +291,11 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	     | _ -> assert false) 
 	  gl
 
-    | IsLetIn _, _ ->
+    | LetIn _, _ ->
 	anomaly "invalid let-in passed to function tcc_aux"
 
     (* fix => tactique Fix *)
-    | IsFix ((ni,_),(fi,ai,_)) , _ ->
+    | Fix ((ni,_),(fi,ai,_)) , _ ->
 	let ids =
 	  Array.to_list
             (Array.map
@@ -309,7 +312,7 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	  gl
 
     (* cofix => tactique CoFix *)
-    | IsCoFix (_,(fi,ai,_)) , _ ->
+    | CoFix (_,(fi,ai,_)) , _ ->
 	let ids =
 	  Array.to_list
             (Array.map
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index ea9e9d104c..f83436e160 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -11,9 +11,11 @@
 open Tacmach
 open Proof_type
 open Libobject
-open Reduction
+open Reductionops
 open Term
+open Termops
 open Names
+open Nameops
 open Util
 open Pp
 open Printer
@@ -22,6 +24,8 @@ open Environ
 open Termast
 open Command
 open Tactics 
+open Safe_typing
+open Nametab
 
 type setoid =
     { set_a : constr;
@@ -39,7 +43,8 @@ type morphism =
 let constr_of c = Astterm.interp_constr Evd.empty (Global.env()) c
 
 let constant dir s =
-  let dir = make_dirpath (List.map id_of_string ("Coq"::"Setoids"::dir)) in
+  let dir = make_dirpath
+              (List.map id_of_string (List.rev ("Coq"::"Setoids"::dir))) in
   let id = id_of_string s in
     try 
       Declare.global_reference_in_absolute_module dir id
@@ -47,7 +52,8 @@ let constant dir s =
     anomaly ("Setoid: cannot find "^(Nametab.string_of_qualid (Nametab.make_qualid dir id)))
 
 let global_constant dir s =
-  let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::dir)) in
+  let dir = make_dirpath
+              (List.map id_of_string (List.rev ("Coq"::"Init"::dir))) in
   let id = id_of_string s in
     try 
       Declare.global_reference_in_absolute_module dir id
@@ -228,14 +234,14 @@ let add_setoid a aeq th =
 	    let eq_ext_name = gen_eq_lem_name () in 
 	    let eq_ext_name2 = gen_eq_lem_name () in 
 	    let _ = Declare.declare_constant eq_ext_name
-		      ((Declare.ConstantEntry {Declarations.const_entry_body = eq_morph; 
-					       Declarations.const_entry_type = None;
-                                               Declarations.const_entry_opaque = true}),
+		      ((Declare.ConstantEntry {const_entry_body = eq_morph; 
+					       const_entry_type = None;
+                                               const_entry_opaque = true}),
 		       Declare.NeverDischarge) in
 	    let _ = Declare.declare_constant eq_ext_name2
-		      ((Declare.ConstantEntry {Declarations.const_entry_body = eq_morph2; 
-					       Declarations.const_entry_type = None;
-                                               Declarations.const_entry_opaque = true}),
+		      ((Declare.ConstantEntry {const_entry_body = eq_morph2; 
+					       const_entry_type = None;
+                                               const_entry_opaque = true}),
 		       Declare.NeverDischarge) in
 	    let eqmorph = (current_constant eq_ext_name) in
 	    let eqmorph2 = (current_constant eq_ext_name2) in
@@ -291,10 +297,10 @@ let check_is_dependent t n =
   in aux t 0 n
 
 let gen_lem_name m = match kind_of_term m with 
-  | IsVar id -> add_suffix id "_ext"
-  | IsConst sp -> add_suffix (basename sp) "_ext"
-  | IsMutInd (sp, i) -> add_suffix (basename sp) ((string_of_int i)^"_ext")
-  | IsMutConstruct ((sp,i),j) -> add_suffix
+  | Var id -> add_suffix id "_ext"
+  | Const sp -> add_suffix (basename sp) "_ext"
+  | Ind (sp, i) -> add_suffix (basename sp) ((string_of_int i)^"_ext")
+  | Construct ((sp,i),j) -> add_suffix
       (basename sp) ((string_of_int i)^(string_of_int i)^"_ext")
   | _ -> errorlabstrm "New Morphism" [< 'sTR "The term "; prterm m; 'sTR "is not a known name">]
 
@@ -453,9 +459,9 @@ let add_morphism lem_name (m,profil) =
 	 (let lem_2 = gen_lem_iff env m mext args_t poss in
 	  let lem2_name = add_suffix lem_name "2" in
 	  let _ = Declare.declare_constant lem2_name
-		    ((Declare.ConstantEntry {Declarations.const_entry_body = lem_2; 
-					     Declarations.const_entry_type = None;
-                                               Declarations.const_entry_opaque = true}),
+		    ((Declare.ConstantEntry {const_entry_body = lem_2; 
+					     const_entry_type = None;
+                                               const_entry_opaque = true}),
 		     Declare.NeverDischarge) in
 	  let lem2 = (current_constant lem2_name) in
 	    (Lib.add_anonymous_leaf
@@ -542,10 +548,10 @@ let get_mark a =
 let rec mark_occur t in_c =
   if (eq_constr t in_c) then Toreplace else
     match kind_of_term in_c with
-      | IsApp (c,al) -> 
+      | App (c,al) -> 
 	  let a = Array.map (mark_occur t) al
 	  in if (get_mark a) then (MApp a) else Tokeep
-      | IsProd (_, c1, c2) -> 
+      | Prod (_, c1, c2) -> 
 	  if (dependent (mkRel 1) c2)
 	  then Tokeep
 	  else 
@@ -599,7 +605,7 @@ let rec create_tac_list i a al c1 c2 hyp args_t = function
 (*      else tclIDTAC::(create_tac_list (i+1) a al c1 c2 hyp q) *)
 
 and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
-  | ((IsApp (c,al)),(MApp a)) -> (
+  | ((App (c,al)),(MApp a)) -> (
       try 
 	let m = morphism_table_find c in
 	let args = Array.of_list (create_args al a m.profil c1 c2) in
@@ -613,7 +619,7 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
 		      tclTHENS (apply (mkApp (xom, args))) (create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil))
       with Not_found -> errorlabstrm "Setoid_replace" 
 	  [< 'sTR "The term "; prterm c; 'sTR " has not been declared as a morphism">])
-  | ((IsProd (_,hh, cc)),(Mimp (hhm, ccm))) ->
+  | ((Prod (_,hh, cc)),(Mimp (hhm, ccm))) ->
       let al = [|hh; cc|] in
       let a = [|hhm; ccm|] in
       let fleche_constr = (Lazy.force coq_fleche) in
@@ -649,7 +655,7 @@ let setoid_replace c1 c2 hyp gl =
 
 let general_s_rewrite lft2rgt c gl =
   let ctype = pf_type_of gl c in
-  let (equiv, args) = decomp_app ctype in
+  let (equiv, args) = decompose_app ctype in
   let rec get_last_two = function
     | [c1;c2] -> (c1, c2)
     | x::y::z -> get_last_two (y::z)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index d9919b7e0d..b71f7ab2a5 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -12,6 +12,7 @@ open Pp
 open Util
 open Names
 open Term
+open Termops
 open Sign
 open Declarations
 open Inductive
@@ -272,13 +273,13 @@ let reduce_to_ind_goal gl t =
   let rec elimrec t =
     let c,args = decomp_app t in
     match kind_of_term c with
-      | IsMutInd (ind_sp,args as ity) -> 
+      | Ind (ind_sp,args as ity) -> 
 	  ((ity, path_of_inductive_path ind_sp, t), t)
-      | IsCast (c,_) when args = [] ->
+      | Cast (c,_) when args = [] ->
 	  elimrec c
-      | IsProd (n,ty,t') when args = [] ->
+      | Prod (n,ty,t') when args = [] ->
 	  let (ind, t) = elimrec t' in (ind, mkProd (n,ty,t))
-      | IsLetIn (n,c,ty,t') when args = [] ->
+      | LetIn (n,c,ty,t') when args = [] ->
 	  let (ind, t) = elimrec t' in (ind, mkLetIn (n,c,ty,t))
       | _ when Instantiate.isEvalRef c ->
 	  elimrec (pf_nf_betaiota gl (pf_one_step_reduce gl t))
@@ -294,7 +295,8 @@ let case_sign ity i =
     | [] -> acc 
     | (c::rest) -> analrec (false::acc) rest
   in
-  let recarg = mis_recarg (lookup_mind_specif ity (Global.env())) in 
+  let (mib,mip) = Global.lookup_inductive ity in
+  let recarg = mip.mind_listrec in 
   analrec [] recarg.(i-1)
 
 let elim_sign ity i =
@@ -306,12 +308,13 @@ let elim_sign ity i =
     | (Mrec k::rest)   -> analrec ((j=k)::acc) rest
     | []               -> List.rev acc 
   in 
-  let recarg = mis_recarg (lookup_mind_specif ity (Global.env())) in
+  let (mib,mip) = Global.lookup_inductive ity in
+  let recarg = mip.mind_listrec in 
   analrec [] recarg.(i-1)
 
 let elimination_sort_of_goal gl = 
   match kind_of_term (hnf_type_of gl (pf_concl gl)) with 
-    | IsSort s ->
+    | Sort s ->
 	(match s with
 	   | Prop Null -> InProp
 	   | Prop Pos -> InSet
@@ -323,7 +326,7 @@ let elimination_sort_of_goal gl =
 (* c should be of type A1->.. An->B with B an inductive definition *)
 
 let last_arg c = match kind_of_term c with
-  | IsApp (f,cl) -> array_last cl
+  | App (f,cl) -> array_last cl
   | _ -> anomaly "last_arg"
 
 let general_elim_then_using 
@@ -336,18 +339,18 @@ let general_elim_then_using
   let elimclause = mk_clenv_from () (elim,w_type_of wc elim) in
   let indmv = 
     match kind_of_term (last_arg (clenv_template elimclause).rebus) with
-      | IsMeta mv -> mv
+      | Meta mv -> mv
       | _         -> error "elimination"
   in
   let pmv =
-    let p, _ = decomp_app (clenv_template_type elimclause).rebus in
+    let p, _ = decompose_app (clenv_template_type elimclause).rebus in
     match kind_of_term p with
-      | IsMeta p -> p
+      | Meta p -> p
       | _ ->
 	  let name_elim =
 	    match kind_of_term elim with
-	      | IsConst sp -> string_of_path sp
-	      | IsVar id -> string_of_id id
+	      | Const sp -> string_of_path sp
+	      | Var id -> string_of_id id
 	      | _ -> "\b"
 	  in
 	  error ("The elimination combinator " ^ name_elim ^ " is not known") 
@@ -355,7 +358,7 @@ let general_elim_then_using
   let elimclause' = clenv_fchain indmv elimclause indclause' in
   let elimclause' = clenv_constrain_with_bindings elimbindings elimclause' in
   let after_tac ce i gl =
-    let (hd,largs) = decomp_app (clenv_template_type ce).rebus in
+    let (hd,largs) = decompose_app (clenv_template_type ce).rebus in
     let branchsign =  elim_sign_fun ity i in
     let ba = { branchsign = branchsign;
                nassums = 
@@ -378,7 +381,8 @@ let general_elim_then_using
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
   let (ind,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
-  let elim = lookup_eliminator (pf_env gl) ind (elimination_sort_of_goal gl) in
+  let elim =
+    Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
   general_elim_then_using
     elim elim_sign tac predicate (indbindings,elimbindings) c gl
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index de1893c3c9..ca22b899b7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -12,10 +12,14 @@ open Pp
 open Util
 open Stamps
 open Names
+open Nameops
 open Sign
 open Term
+open Termops
+open Declarations
 open Inductive
-open Reduction
+open Inductiveops
+open Reductionops
 open Environ
 open Declare
 open Evd
@@ -30,15 +34,16 @@ open Clenv
 open Tacticals
 open Hipattern
 open Coqlib
+open Nametab
 
 exception Bound
 
 let rec nb_prod x =
   let rec count n c =
     match kind_of_term c with
-        IsProd(_,_,t) -> count (n+1) t
-      | IsLetIn(_,a,_,t) -> count n (subst1 a t)
-      | IsCast(c,_) -> count n c
+        Prod(_,_,t) -> count (n+1) t
+      | LetIn(_,a,_,t) -> count n (subst1 a t)
+      | Cast(c,_) -> count n c
       | _ -> n
   in count 0 x
 
@@ -59,23 +64,23 @@ let get_pairs_from_bindings =
 
 let string_of_inductive c = 
   try match kind_of_term c with
-  | IsMutInd ind_sp -> 
-      let mispec = Global.lookup_mind_specif ind_sp in 
-      string_of_id (mis_typename mispec)
+  | Ind ind_sp -> 
+      let (mib,mip) = Global.lookup_inductive ind_sp in 
+      string_of_id mip.mind_typename
   | _ -> raise Bound
   with Bound -> error "Bound head variable"
 
 let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
   match kind_of_term t with
-    | IsProd (_,_,c2)  -> head_constr_bound c2 l 
-    | IsLetIn (_,_,_,c2) -> head_constr_bound c2 l 
-    | IsApp (f,args)  -> 
+    | Prod (_,_,c2)  -> head_constr_bound c2 l 
+    | LetIn (_,_,_,c2) -> head_constr_bound c2 l 
+    | App (f,args)  -> 
 	head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
-    | IsConst _        -> t::l
-    | IsMutInd _       -> t::l
-    | IsMutConstruct _ -> t::l
-    | IsVar _          -> t::l
+    | Const _        -> t::l
+    | Ind _       -> t::l
+    | Construct _ -> t::l
+    | Var _          -> t::l
     | _                -> raise Bound
 
 let head_constr c = 
@@ -161,7 +166,7 @@ let reduct_in_hyp redfun idref gl =
   let inhyp,id = match idref with
     | InHyp id -> true, id
     | InHypType id -> false, id in
-  let c, ty = pf_get_hyp gl id in
+  let (_,c, ty) = pf_get_hyp gl id in
   let redfun' = under_casts (pf_reduce redfun gl) in
   match c with
     | None -> convert_hyp id (redfun' ty) gl
@@ -247,7 +252,7 @@ let dyn_reduce = function
 
 let unfold_constr = function 
   | ConstRef sp -> unfold_in_concl [[],Closure.EvalConstRef sp]
-  | VarRef sp -> unfold_in_concl [[],Closure.EvalVarRef (basename sp)]
+  | VarRef id -> unfold_in_concl [[],Closure.EvalVarRef id]
   | _ -> errorlabstrm "unfold_constr" [< 'sTR "Cannot unfold a non-constant.">]
 
 (*******************************************)
@@ -280,12 +285,12 @@ let id_of_name_with_default s = function
 
 let default_id gl =
   match kind_of_term (strip_outer_cast (pf_concl gl)) with
-    | IsProd (name,c1,c2) ->
+    | Prod (name,c1,c2) ->
   	(match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl c1)) with
-	   | IsSort (Prop _) -> (id_of_name_with_default "H" name)
-	   | IsSort (Type _) -> (id_of_name_with_default "X" name)
+	   | Sort (Prop _) -> (id_of_name_with_default "H" name)
+	   | Sort (Type _) -> (id_of_name_with_default "X" name)
 	   | _                   -> anomaly "Wrong sort")
-    | IsLetIn (name,b,_,_) -> id_of_name_using_hdchar (pf_env gl) b name
+    | LetIn (name,b,_,_) -> id_of_name_using_hdchar (pf_env gl) b name
     | _ -> raise (RefinerError IntroNeedsProduct)
 
 (* Non primitive introduction tactics are treated by central_intro
@@ -424,7 +429,7 @@ let hide_ident_or_numarg_tactic s tac =
 let intros_do n g = 
   let depth = 
     let rec lookup all nodep c = match kind_of_term c with
-      | IsProd (name,_,c') -> 
+      | Prod (name,_,c') -> 
 	  (match name with
 	     | Name(s')  -> 
 		 if dependent (mkRel 1) c' then 
@@ -435,7 +440,7 @@ let intros_do n g =
 		   lookup (all+1) (nodep+1) c'
              | Anonymous -> 
 		 if nodep=n then all else lookup (all+1) (nodep+1) c')
-      | IsCast (c,_) -> lookup all nodep c
+      | Cast (c,_) -> lookup all nodep c
       | _ -> error "No such hypothesis in current goal"
     in 
     lookup 1 1 (pf_concl g)
@@ -507,7 +512,7 @@ let bring_hyps ids gl =
 let apply_with_bindings  (c,lbind) gl = 
   let apply = 
     match kind_of_term c with 
-      | IsLambda _ -> res_pf_cast 
+      | Lambda _ -> res_pf_cast 
       | _ -> res_pf 
   in 
   let (wc,kONT) = startWalk gl in
@@ -566,7 +571,7 @@ let dyn_apply l =
 let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
   match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
-    | IsProd (_,c1,c2) when not (dependent (mkRel 1) c2) ->
+    | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
 	tclTHENS 
 	  (apply_type (mkProd (Anonymous,c2,goal_constr))
 	     [mkMeta (new_meta())])
@@ -584,12 +589,12 @@ let dyn_cut_and_apply = function
 
 let true_cut id c gl =
   match kind_of_term (hnf_type_of gl c) with
-    | IsSort _ -> internal_cut id c gl
+    | Sort _ -> internal_cut id c gl
     | _  -> error "Not a proposition or a type"
 
 let true_cut_anon c gl =
   match kind_of_term (hnf_type_of gl c) with
-    | IsSort s -> 
+    | Sort s -> 
         let d = match s with Prop _ -> "H" | Type _ -> "X" in
         let id = next_name_away_with_default d Anonymous (pf_ids_of_hyps gl) in
         internal_cut id c gl
@@ -604,7 +609,7 @@ let dyn_true_cut = function
 
 let cut c gl =
   match kind_of_term (hnf_type_of gl c) with
-    | IsSort _ ->
+    | Sort _ ->
         let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
         let t = mkProd (Anonymous, c, pf_concl gl) in
         tclTHENS
@@ -641,7 +646,7 @@ let cut_in_parallel l =
 let generalize_goal gl c cl =
   let t = pf_type_of gl c in
   match kind_of_term c with
-    | IsVar id -> mkNamedProd id t cl
+    | Var id -> mkNamedProd id t cl
     | _        -> 
         let cl' = subst_term c cl in 
         if noccurn 1 cl' then 
@@ -668,7 +673,7 @@ let generalize_dep c gl =
   let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
   let tothin' =
     match kind_of_term c with
-      | IsVar id when mem_named_context id sign & not (List.mem id init_ids)
+      | Var id when mem_named_context id sign & not (List.mem id init_ids)
 	  -> id::tothin
       | _ -> tothin
   in
@@ -955,7 +960,8 @@ let dyn_move_dep = function
 let constructor_checking_bound  boundopt i lbind gl =
   let cl = pf_concl gl in 
   let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in 
-  let nconstr = mis_nconstr (Global.lookup_mind_specif mind) 
+  let nconstr =
+    Array.length (snd (Global.lookup_inductive mind)).mind_consnames
   and sigma   = project gl in
   if i=0 then error "The constructors are numbered starting from 1";
   if i > nconstr then error "Not enough constructors";
@@ -965,7 +971,7 @@ let constructor_checking_bound  boundopt i lbind gl =
 	  error "Not the expected number of constructors"
     | None -> ()
   end;
-  let cons = mkMutConstruct (ith_constructor_of_inductive mind i) in
+  let cons = mkConstruct (ith_constructor_of_inductive mind i) in
   let apply_tac = apply_with_bindings (cons,lbind) in
   (tclTHENLIST [convert_concl redcl; intros; apply_tac]) gl
 
@@ -974,7 +980,8 @@ let one_constructor i = (constructor_checking_bound None i)
 let any_constructor gl = 
   let cl = pf_concl gl in 
   let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in
-  let nconstr = mis_nconstr (Global.lookup_mind_specif mind)
+  let nconstr =
+    Array.length (snd (Global.lookup_inductive mind)).mind_consnames
   and sigma   = project gl in
   if nconstr = 0 then error "The type has no constructors";
   tclFIRST (List.map (fun i -> one_constructor i []) 
@@ -1024,13 +1031,13 @@ let dyn_split  = function
 *)
 
 let last_arg c = match kind_of_term c with
-  | IsApp (f,cl) ->  array_last cl
+  | App (f,cl) ->  array_last cl
   | _ -> anomaly "last_arg"
 	
 let elimination_clause_scheme kONT wc elimclause indclause gl = 
   let indmv = 
     (match kind_of_term (last_arg (clenv_template elimclause).rebus) with
-       | IsMeta mv -> mv
+       | Meta mv -> mv
        | _  -> errorlabstrm "elimination_clause"
              [< 'sTR "The type of elimination clause is not well-formed" >]) 
   in
@@ -1067,19 +1074,8 @@ let default_elim (c,lbindc)  gl =
   let env = pf_env gl in
   let (ind,t) = reduce_to_quantified_ind env (project gl) (pf_type_of gl c) in
   let s = elimination_sort_of_goal gl in
-  let elimc =
-    try lookup_eliminator env ind s 
-    with Not_found -> 
-      let dir, base,k = repr_path (path_of_inductive_path ind) in
-      let id = make_elimination_ident base s in
-      errorlabstrm "default_elim"
-	[< 'sTR "Cannot find the elimination combinator :";
-           pr_id id; 'sPC;
-	   'sTR "The elimination of the inductive definition :";
-           pr_id base; 'sPC; 'sTR "on sort "; 
-           'sPC; print_sort (new_sort_in_family s) ;
-	   'sTR " is probably not allowed" >]
-  in  general_elim (c,lbindc) (elimc,[]) gl
+  let elimc = Indrec.lookup_eliminator ind s in
+  general_elim (c,lbindc) (elimc,[]) gl
 
 
 (* The simplest elimination tactic, with no substitutions at all. *)
@@ -1124,13 +1120,13 @@ comes from a canonically generated one *)
 let rec is_rec_arg env sigma indpath t =
   try
     let (ind_sp,_) = find_mrectype env sigma t in
-    Declare.path_of_inductive_path ind_sp = indpath
+    path_of_inductive env ind_sp = indpath
   with Induc -> 
     false
 
 let rec recargs indpath env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
-    | IsProd (na,t,c2) ->
+    | Prod (na,t,c2) ->
 	(is_rec_arg env sigma indpath t)
 	::(recargs indpath (push_rel_assum (na,t) env) sigma c2)
     | _ -> []
@@ -1149,7 +1145,7 @@ let induct_discharge old_style mind statuslists cname destopt avoid ra gl =
   let hyprecname =
     add_prefix indhyp 
       (if old_style || atompart_of_id recvarname <> "H" then recvarname
-       else mis_typename (lookup_mind_specif mind (Global.env())))
+       else (snd (Global.lookup_inductive mind)).mind_typename)
   in
   let avoid =
     if old_style then avoid
@@ -1190,10 +1186,10 @@ let induct_discharge old_style mind statuslists cname destopt avoid ra gl =
 let atomize_param_of_ind hyp0 gl =
   let tmptyp0 = pf_get_hyp_typ gl hyp0 in
   let (mind,typ0) = pf_reduce_to_quantified_ind gl tmptyp0 in
-  let mis = Global.lookup_mind_specif mind in
-  let nparams = mis_nparams mis in
+  let (mib,mip) = Global.lookup_inductive mind in
+  let nparams = mip.mind_nparams in
   let prods, indtyp = decompose_prod typ0 in
-  let argl = snd (decomp_app indtyp) in
+  let argl = snd (decompose_app indtyp) in
   let params = list_firstn nparams argl in
   (* le gl est important pour ne pas préévaluer *)
   let rec atomize_one i avoid gl =
@@ -1202,12 +1198,12 @@ let atomize_param_of_ind hyp0 gl =
       (* If argl <> [], we expect typ0 not to be quantified, in order to
          avoid bound parameters... then we call pf_reduce_to_atomic_ind *)
       let (_,indtyp) = pf_reduce_to_atomic_ind gl tmptyp0 in
-      let argl = snd (decomp_app indtyp) in
+      let argl = snd (decompose_app indtyp) in
       let c = List.nth argl (i-1) in
       match kind_of_term c with
-	| IsVar id when not (List.exists (occur_var (pf_env gl) id) avoid) ->
+	| Var id when not (List.exists (occur_var (pf_env gl) id) avoid) ->
 	    atomize_one (i-1) ((mkVar id)::avoid) gl
-	| IsVar id ->
+	| Var id ->
 	    let x = fresh_id [] id gl in
 	    tclTHEN
 	      (letin_tac true (Name x) (mkVar id) (None,[]))
@@ -1225,15 +1221,15 @@ let atomize_param_of_ind hyp0 gl =
   atomize_one (List.length argl) params gl
 
 let find_atomic_param_of_ind mind indtyp =
-  let mis = Global.lookup_mind_specif mind in
-  let nparams = mis_nparams mis in
-  let argl = snd (decomp_app indtyp) in
+  let (mib,mip) = Global.lookup_inductive mind in
+  let nparams = mip.mind_nparams in
+  let argl = snd (decompose_app indtyp) in
   let argv = Array.of_list argl in
   let params = list_firstn nparams argl in
   let indvars = ref Idset.empty in
   for i = nparams to (Array.length argv)-1 do
     match kind_of_term argv.(i) with
-      | IsVar id
+      | Var id
           when not (List.exists (occur_var (Global.env()) id) params) -> 
 	  indvars := Idset.add id !indvars
       | _ -> ()
@@ -1389,28 +1385,28 @@ let induction_tac varname typ (elimc,elimt) gl =
   elimination_clause_scheme kONT wc elimclause indclause gl
 
 let is_indhyp p n t =
-  let c,_ = decomp_app t in 
+  let c,_ = decompose_app t in 
   match kind_of_term c with
-    | IsRel k when p < k & k <= p + n -> true
+    | Rel k when p < k & k <= p + n -> true
     | _ -> false
 
 (* We check that the eliminator has been build by Coq (usual *)
 (* eliminator _ind, _rec or _rect, or eliminator built by Scheme) *)
 let compute_elim_signature_and_roughly_check elimt mind =
-  let mis = Global.lookup_mind_specif mind in
-  let lra = mis_recarg mis in
-  let nconstr = mis_nconstr mis in
-  let _,elimt2 = decompose_prod_n (mis_nparams mis) elimt in
+  let (mib,mip) = Global.lookup_inductive mind in
+  let lra = mip.mind_listrec in
+  let nconstr = Array.length mip.mind_consnames in
+  let _,elimt2 = decompose_prod_n mip.mind_nparams elimt in
   let n = nb_prod elimt2 in
-  let npred = n - nconstr - (mis_nrealargs mis) - 1 in
+  let npred = n - nconstr - mip.mind_nrealargs - 1 in
   let rec check_branch p c ra = match kind_of_term c, ra with
-    | IsProd (_,_,c), Declarations.Mrec i :: ra' ->
+    | Prod (_,_,c), Declarations.Mrec i :: ra' ->
 	(match kind_of_term c with
-	   | IsProd (_,t,c) when is_indhyp (p+1) npred t ->
+	   | Prod (_,t,c) when is_indhyp (p+1) npred t ->
 	       true::(check_branch (p+2) c ra')
 	   | _ -> false::(check_branch (p+1) c ra'))
-    | IsLetIn (_,_,_,c), ra' -> false::(check_branch (p+1) c ra)
-    | IsProd (_,_,c), _ :: ra -> false::(check_branch (p+1) c ra)
+    | LetIn (_,_,_,c), ra' -> false::(check_branch (p+1) c ra)
+    | Prod (_,_,c), _ :: ra -> false::(check_branch (p+1) c ra)
     | _, [] -> []
     | _ ->
 	error"Not a recursive eliminator: some constructor argument is lacking"
@@ -1418,7 +1414,7 @@ let compute_elim_signature_and_roughly_check elimt mind =
   let rec check_elim c n =
     if n = nconstr then []
     else match kind_of_term c with
-    | IsProd (_,t,c) -> (check_branch n t lra.(n)) :: (check_elim c (n+1))
+    | Prod (_,t,c) -> (check_branch n t lra.(n)) :: (check_elim c (n+1))
     | _ -> error "Not an eliminator: some constructor case is lacking" in
   let _,elimt3 = decompose_prod_n npred elimt2 in
   check_elim elimt3 0
@@ -1433,7 +1429,7 @@ let induction_from_context isrec style hyp0 gl =
   let (mind,typ0) = pf_reduce_to_quantified_ind gl tmptyp0 in
   let indvars = find_atomic_param_of_ind mind (snd (decompose_prod typ0)) in
   let elimc =
-    if isrec then lookup_eliminator env mind (elimination_sort_of_goal gl)
+    if isrec then Indrec.lookup_eliminator mind (elimination_sort_of_goal gl)
     else Indrec.make_case_gen env (project gl) mind (elimination_sort_of_goal gl)
   in
   let elimt = pf_type_of gl elimc in
@@ -1476,7 +1472,7 @@ let induction_with_atomization_of_ind_arg isrec hyp0 =
 
 let new_induct isrec c gl =
   match kind_of_term c with
-    | IsVar id when not (mem_named_context id (Global.named_context())) ->
+    | Var id when not (mem_named_context id (Global.named_context())) ->
 	induction_with_atomization_of_ind_arg isrec id gl
     | _        ->
 	let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) 
@@ -1592,7 +1588,7 @@ let elim_scheme_type elim t gl =
   let (wc,kONT) = startWalk gl in
   let clause = mk_clenv_type_of wc elim in 
   match kind_of_term (last_arg (clenv_template clause).rebus) with
-    | IsMeta mv ->
+    | Meta mv ->
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
 	  clenv_unify CUMUL t (clenv_instance_type clause mv) clause in
@@ -1601,7 +1597,7 @@ let elim_scheme_type elim t gl =
 
 let elim_type t gl =
   let (ind,t) = pf_reduce_to_atomic_ind gl t in
-  let elimc = lookup_eliminator (pf_env gl) ind (elimination_sort_of_goal gl) in
+  let elimc = Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
   elim_scheme_type elimc t gl
 
 let dyn_elim_type = function
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 75235b6577..d494417753 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -20,6 +20,7 @@ open Evar_refiner
 open Clenv
 open Tacred
 open Tacticals
+open Nametab
 (*i*)
 
 (* Main tactics. *)
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 6672e56c4f..2d0f49f4ec 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -10,9 +10,11 @@
 
 open Util
 open Names
+open Nameops
 open Term
 open Pattern
 open Rawterm
+open Nametab
 
 (* Discrimination nets of terms.
    See the module dn.ml for further explanations.
@@ -24,8 +26,8 @@ type 'a t = (constr_label,constr_pattern,'a) Dn.t
 
 let decomp = 
   let rec decrec acc c = match kind_of_term c with
-    | IsApp (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
-    | IsCast (c1,_) -> decrec acc c1
+    | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
+    | Cast (c1,_) -> decrec acc c1
     | _ -> (c,acc)
   in 
   decrec []
@@ -44,17 +46,17 @@ let constr_pat_discr t =
     match decomp_pat t with
       | PRef (IndRef sp), args -> Some(IndNode sp,args)
       | PRef (ConstructRef sp), args -> Some(CstrNode sp,args)
-      | PRef (VarRef sp), args -> Some(VarNode (basename sp),args)
+      | PRef (VarRef id), args -> Some(VarNode id,args)
       | _ -> None
 
 let constr_val_discr t =
   let c, l = decomp t in
   match kind_of_term c with
-    (* IsConst _,_) -> Some(TERM c,l) *)
-    | IsMutInd ind_sp -> Some(IndNode ind_sp,l)
-    | IsMutConstruct cstr_sp -> Some(CstrNode cstr_sp,l)
+    (* Const _,_) -> Some(TERM c,l) *)
+    | Ind ind_sp -> Some(IndNode ind_sp,l)
+    | Construct cstr_sp -> Some(CstrNode cstr_sp,l)
     (* Ici, comment distinguer SectionVarNode de VarNode ?? *)
-    | IsVar id -> Some(VarNode id,l)
+    | Var id -> Some(VarNode id,l)
     | _ -> None
 
 (* Les deux fonctions suivantes ecrasaient les precedentes, 
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 2c791f3bbf..0df646c0c4 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -11,9 +11,11 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
+open Termops
 open Sign
-open Reduction
+open Reductionops
 open Environ
 open Logic
 open Tacmach
@@ -99,10 +101,10 @@ let clenv_constrain_with_bindings bl clause =
 
 let add_prod_rel sigma (t,env) =
   match kind_of_term t with
-    | IsProd (na,t1,b) ->
+    | Prod (na,t1,b) ->
         (b,push_rel_assum (na, t1) env)
-    | IsLetIn (na,c1,t1,b) ->
-        (b,push_rel_def (na,c1, t1) env)
+    | LetIn (na,c1,t1,b) ->
+        (b,push_rel (na,Some c1, t1) env)
     | _ -> failwith "add_prod_rel"
 
 let rec add_prods_rel sigma (t,env) =
@@ -127,20 +129,20 @@ let elim_res_pf_THEN_i kONT clenv tac gls =
 
 let rec build_args acc ce p_0 p_1 =
   match kind_of_term p_0, p_1 with 
-    | (IsProd (na,a,b), (a_0::bargs)) ->
+    | (Prod (na,a,b), (a_0::bargs)) ->
         let (newa,ce') = (build_term ce (na,Some a) a_0) in 
 	build_args (newa::acc) ce' (subst1 a_0 b) bargs
-    | (IsLetIn (na,a,t,b), args) -> build_args acc ce (subst1 a b) args
+    | (LetIn (na,a,t,b), args) -> build_args acc ce (subst1 a b) args
     | (_, [])     -> (List.rev acc,ce)
     | (_, (_::_)) -> failwith "mk_clenv_using"
 
 and build_term ce p_0 c =
   let env = w_env ce.hook in
   match p_0, kind_of_term c with 
-    | ((na,Some t), IsMeta mv) -> 
+    | ((na,Some t), Meta mv) -> 
 (*    	let mv = new_meta() in *)
 	(mkMeta mv, clenv_pose (na,mv,t) ce)
-    | ((na,_), IsCast (c,t)) -> build_term ce (na,Some t) c
+    | ((na,_), Cast (c,t)) -> build_term ce (na,Some t) c
     | ((na,Some t), _) ->
     	if (not((occur_meta c))) then 
 	  (c,ce)
@@ -169,7 +171,7 @@ and build_term ce p_0 c =
 	  (newc,ce')
 
 let mk_clenv_using wc c =
-  let ce = mk_clenv wc mkImplicit in
+  let ce = mk_clenv wc mkProp in
   let (newc,ce') = 
     try 
       build_term ce (Anonymous,None) c
@@ -192,11 +194,11 @@ let clenv_apply_n_times n ce =
     match (n, kind_of_term templtyp) with 
       | (0, _) ->
 	  clenv_change_head (applist(templval,List.rev argacc), templtyp) ce
-      | (n, IsProd (na,dom,rng)) ->
+      | (n, Prod (na,dom,rng)) ->
           let mv = new_meta() in
           let newce = clenv_pose (na,mv,dom) ce in
 	  apprec newce (mkMeta mv::argacc) (n-1, subst1 (mkMeta mv) rng)
-      | (n, IsLetIn (na,b,t,c)) ->
+      | (n, LetIn (na,b,t,c)) ->
 	  apprec ce argacc (n, subst1 b c)
       | (n, _) -> failwith "clenv_apply_n_times"
   in