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

14 files changed, 146 insertions, 129 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index c2aa9a7ff..4ea4c4f50 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -12,13 +12,14 @@ open Pp
 open Util
 open Names
 open Term
+open Termops
 open Sign
 open Instantiate
 open Environ
 open Evd
 open Proof_type
 open Logic
-open Reduction
+open Reductionops
 open Tacmach
 open Evar_refiner
 
@@ -39,7 +40,7 @@ let exist_to_meta (emap, c) =
   List.iter add_binding emap;
   let rec replace c =
     match kind_of_term c with
-        IsEvar k -> List.assoc k !subst
+        Evar k -> List.assoc k !subst
       | _ -> map_constr replace c in
   (!mmap, replace c)
 
@@ -66,7 +67,7 @@ let applyHead n c wc =
       (wc,c)
     else 
       match kind_of_term (w_whd_betadeltaiota wc cty) with
-        | IsProd (_,c1,c2) ->
+        | Prod (_,c1,c2) ->
 	    let evar = Evarutil.new_evar_in_sign (w_env wc) in
             let (evar_n, _) = destEvar evar in
 	    (compose 
@@ -99,20 +100,20 @@ let unify_0 cv_pb mc wc m n =
     and cN = Evarutil.whd_castappevar sigma n in 
     try 
       match (kind_of_term cM,kind_of_term cN) with
-	| IsCast (c,_), _ -> unirec_rec pb substn c cN
-	| _, IsCast (c,_) -> unirec_rec pb substn cM c
-	| IsMeta k1, IsMeta k2 ->
+	| Cast (c,_), _ -> unirec_rec pb substn c cN
+	| _, Cast (c,_) -> unirec_rec pb substn cM c
+	| Meta k1, Meta k2 ->
 	    if k1 < k2 then (k1,cN)::metasubst,evarsubst
 	    else if k1 = k2 then substn
 	    else (k2,cM)::metasubst,evarsubst
-	| IsMeta k, _    -> (k,cN)::metasubst,evarsubst
-	| _, IsMeta k    -> (k,cM)::metasubst,evarsubst
-	| IsLambda (_,t1,c1), IsLambda (_,t2,c2) ->
+	| Meta k, _    -> (k,cN)::metasubst,evarsubst
+	| _, Meta k    -> (k,cM)::metasubst,evarsubst
+	| Lambda (_,t1,c1), Lambda (_,t2,c2) ->
 	    unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2
-	| IsProd (_,t1,c1), IsProd (_,t2,c2) ->
+	| Prod (_,t1,c1), Prod (_,t2,c2) ->
 	    unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2
 
-	| IsApp (f1,l1), IsApp (f2,l2) ->
+	| App (f1,l1), App (f2,l2) ->
 	    let len1 = Array.length l1
 	    and len2 = Array.length l2 in
 	    if len1 = len2 then
@@ -129,42 +130,42 @@ let unify_0 cv_pb mc wc m n =
 		(unirec_rec CONV substn (appvect (f1,extras)) f2)
                 restl1 l2
 		
-	| IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) ->
+	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             array_fold_left2 (unirec_rec CONV)
 	      (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2
 		
-	| IsMutConstruct _, IsMutConstruct _ ->
+	| Construct _, Construct _ ->
 	    if is_conv env sigma cM cN then
 	      substn
 	    else
-	      error_cannot_unify CCI (m,n)
+	      error_cannot_unify (m,n)
 	      
-	| IsMutInd _, IsMutInd _ ->
+	| Ind _, Ind _ ->
 	    if is_conv env sigma  cM cN then
 	      substn
 	    else
-	      error_cannot_unify CCI (m,n)
+	      error_cannot_unify (m,n)
 	      
-	| IsEvar _, _ ->
+	| Evar _, _ ->
 	    metasubst,((cM,cN)::evarsubst)
-	| _, IsEvar _ ->
+	| _, Evar _ ->
 	    metasubst,((cN,cM)::evarsubst)
 
-	| (IsConst _ | IsVar _ | IsRel _), _ ->
+	| (Const _ | Var _ | Rel _), _ ->
 	    if is_conv env sigma cM cN then
 	      substn
 	    else 
-	      error_cannot_unify CCI (m,n)
+	      error_cannot_unify (m,n)
 		
-	| _, (IsConst _ | IsVar _| IsRel _) ->
+	| _, (Const _ | Var _| Rel _) ->
 	    if (not (occur_meta cM)) & is_conv env sigma cM cN then 
 	      substn
 	    else 
-	      error_cannot_unify CCI (m,n)
+	      error_cannot_unify (m,n)
 
-	| IsLetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
+	| LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
 		
-	| _ -> error_cannot_unify CCI (m,n)
+	| _ -> error_cannot_unify (m,n)
 	      
     with ex when catchable_exception ex ->
       if (not(occur_meta cM)) & is_fconv pb env sigma cM cN then 
@@ -239,12 +240,12 @@ and w_resrec metas evars wc =
     | (lhs,rhs) :: t ->
     match kind_of_term rhs with
 
-      | IsMeta k -> w_resrec ((k,lhs)::metas) t wc
+      | Meta k -> w_resrec ((k,lhs)::metas) t wc
 
       | krhs ->
       match kind_of_term lhs with
 
-	| IsEvar (evn,_) ->
+	| Evar (evn,_) ->
 	    if w_defined_evar wc evn then
 	      let (wc',metas') = w_Unify CONV rhs lhs metas wc in 
 	      w_resrec metas' t wc'
@@ -253,7 +254,7 @@ and w_resrec metas evars wc =
 		 w_resrec metas t (w_Define evn rhs wc)
                with ex when catchable_exception ex ->
 		 (match krhs with
-             	    | IsApp (f,cl) when isConst f ->
+             	    | App (f,cl) when isConst f ->
 			let wc' = mimick_evar f (Array.length cl) evn wc in
 			w_resrec metas evars wc'
 		    | _ -> error "w_Unify"))
@@ -276,7 +277,7 @@ let unify m gls =
 let collect_metas 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
   List.rev (collrec [] c)
@@ -284,7 +285,7 @@ let collect_metas c =
 let metavars_of c =  
   let rec collrec acc c =
     match kind_of_term c with
-      | IsMeta mv -> Intset.add mv acc
+      | Meta mv -> Intset.add mv acc
       | _         -> fold_constr collrec acc c
   in 
   collrec Intset.empty c
@@ -326,8 +327,8 @@ let clenv_environments bound c =
   let rec clrec (ne,e,metas) n c =
     match n, kind_of_term c with
       | (0, _) -> (ne, e, List.rev metas, c)
-      | (n, IsCast (c,_)) -> clrec (ne,e,metas) n c
-      | (n, IsProd (na,c1,c2)) ->
+      | (n, Cast (c,_)) -> clrec (ne,e,metas) n c
+      | (n, Prod (na,c1,c2)) ->
 	  let mv = new_meta () in
 	  let dep = dependent (mkRel 1) c2 in
 	  let ne' =
@@ -347,7 +348,7 @@ let clenv_environments bound c =
 	  let e' = Intmap.add mv (Cltyp (mk_freelisted c1)) e in 
 	  clrec (ne',e', (mkMeta mv)::metas) (n-1)
 	    (if dep then (subst1 (mkMeta mv) c2) else c2)
-      | (n, IsLetIn (na,b,_,c)) -> clrec (ne,e,metas) (n-1) (subst1 b c)
+      | (n, LetIn (na,b,_,c)) -> clrec (ne,e,metas) (n-1) (subst1 b c)
       | (n, _) -> (ne, e, List.rev metas, c)
   in 
   clrec (Intmap.empty,Intmap.empty,[]) bound c
@@ -463,13 +464,13 @@ let clenv_instance_term clenv c =
 let clenv_cast_meta clenv = 
   let rec crec u =
     match kind_of_term u with
-      | IsApp _ | IsMutCase _ -> crec_hd u
-      | IsCast (c,_) when isMeta c -> u
+      | App _ | Case _ -> crec_hd u
+      | Cast (c,_) when isMeta c -> u
       | _  -> map_constr crec u
 	    
   and crec_hd u =
     match kind_of_term (strip_outer_cast u) with
-      | IsMeta mv ->
+      | Meta mv ->
 	  (try 
 	     match Intmap.find mv clenv.env with
                | Cltyp b ->
@@ -478,9 +479,9 @@ let clenv_cast_meta clenv =
 	       | Clval(_) -> u
 	   with Not_found -> 
 	     u)
-      | IsApp(f,args) -> mkApp (crec_hd f, Array.map crec args)
-      | IsMutCase(ci,p,c,br) ->
-	  mkMutCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+      | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
+      | Case(ci,p,c,br) ->
+	  mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
       | _ -> u
   in 
   crec
@@ -564,12 +565,12 @@ let clenv_merge with_types =
       | ((lhs,rhs)::t, metas) ->
       (match kind_of_term rhs with
 
-	| IsMeta k -> clenv_resrec ((k,lhs)::metas) t clenv
+	| Meta k -> clenv_resrec ((k,lhs)::metas) t clenv
 
 	| krhs ->
         (match kind_of_term lhs with
 
-	  | IsEvar (evn,_) ->
+	  | Evar (evn,_) ->
     	      if w_defined_evar clenv.hook evn then
 		let (metas',evars') = unify_0 CONV [] clenv.hook rhs lhs in
 		clenv_resrec (metas'@metas) (evars'@t) clenv
@@ -583,7 +584,7 @@ let clenv_merge with_types =
 		    (clenv_wtactic (w_Define evn rhs') clenv)
 		with ex when catchable_exception ex ->
 		  (match krhs with
-		     | IsApp (f,cl) when isConst f or isMutConstruct f ->
+		     | App (f,cl) when isConst f or isConstruct f ->
 			 clenv_resrec metas evars 
 			   (clenv_wtactic
 			      (mimick_evar f (Array.length cl) evn)
@@ -728,7 +729,7 @@ let constrain_clenv_to_subterm clause (op,cl) =
        else error "Bound 1"
      with ex when catchable_exception ex ->
        (match kind_of_term cl with 
-	  | IsApp (f,args) ->
+	  | App (f,args) ->
 	      let n = Array.length args in
 	      assert (n>0);
 	      let c1 = mkApp (f,Array.sub args 0 (n-1)) in
@@ -737,35 +738,35 @@ let constrain_clenv_to_subterm clause (op,cl) =
 		 matchrec c1
 	       with ex when catchable_exception ex -> 
 		 matchrec c2)
-          | IsMutCase(_,_,c,lf) -> (* does not search in the predicate *)
+          | Case(_,_,c,lf) -> (* does not search in the predicate *)
 	       (try 
 		 matchrec c
 	       with ex when catchable_exception ex -> 
 		 iter_fail matchrec lf)
-	  | IsLetIn(_,c1,_,c2) -> 
+	  | LetIn(_,c1,_,c2) -> 
 	       (try 
 		 matchrec c1
 	       with ex when catchable_exception ex -> 
 		 matchrec c2)
 
-	  | IsFix(_,(_,types,terms)) -> 
+	  | Fix(_,(_,types,terms)) -> 
 	       (try 
 		 iter_fail matchrec types
 	       with ex when catchable_exception ex -> 
 		 iter_fail matchrec terms)
 	
-	  | IsCoFix(_,(_,types,terms)) -> 
+	  | CoFix(_,(_,types,terms)) -> 
 	       (try 
 		 iter_fail matchrec types
 	       with ex when catchable_exception ex -> 
 		 iter_fail matchrec terms)
 
-          | IsProd (_,t,c) ->
+          | Prod (_,t,c) ->
 	      (try 
 		 matchrec t 
 	       with ex when catchable_exception ex -> 
 		 matchrec c)
-          | IsLambda (_,t,c) ->
+          | Lambda (_,t,c) ->
 	      (try 
 		 matchrec t 
 	       with ex when catchable_exception ex -> 
@@ -1007,7 +1008,7 @@ let secondOrderAbstraction allow_K gl p oplist clause =
 let clenv_so_resolver allow_K clause gl =
   let c, oplist = whd_stack (clenv_instance_template_type clause) in
   match kind_of_term c with
-    | IsMeta p ->
+    | Meta p ->
 	let clause' = secondOrderAbstraction allow_K gl p oplist clause in 
 	clenv_fo_resolver clause' gl
     | _ -> error "clenv_so_resolver"
@@ -1027,7 +1028,7 @@ let clenv_unique_resolver allow_K clenv gls =
   let pathd,_ = whd_stack (clenv_instance_template_type clenv) in
   let glhd,_ = whd_stack (pf_concl gls) in
   match kind_of_term pathd, kind_of_term glhd with
-    | IsMeta _, IsLambda _ ->
+    | Meta _, Lambda _ ->
 	(try 
 	   clenv_typed_fo_resolver clenv gls
 	 with ex when catchable_exception ex -> 
@@ -1036,7 +1037,7 @@ let clenv_unique_resolver allow_K clenv gls =
 	   with ex when catchable_exception ex -> 
 	     error "Cannot solve a second-order unification problem")
 
-    | IsMeta _, _ -> 
+    | Meta _, _ -> 
 	(try 
 	   clenv_so_resolver allow_K clenv gls
          with ex when catchable_exception ex -> 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f402e964d..65307debe 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -56,7 +56,7 @@ type wc = walking_constraints (* for a better reading of the following *)
 
 val unify : constr -> tactic
 val unify_0 : 
-  Reduction.conv_pb -> (int * constr) list -> wc -> constr -> constr 
+  Reductionops.conv_pb -> (int * constr) list -> wc -> constr -> constr 
     -> (int * constr) list * (constr * constr) list
 
 val collect_metas : constr -> int list
@@ -80,7 +80,7 @@ val clenv_instance_type : wc clausenv -> int -> constr
 val clenv_instance_template : wc clausenv -> constr
 val clenv_instance_template_type : wc clausenv -> constr
 val clenv_unify : 
-  Reduction.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
+  Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
 val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
 val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
 val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
@@ -120,7 +120,7 @@ val clenv_constrain_dep_args_of :
 val constrain_clenv_using_subterm_list : 
   bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list
 val clenv_typed_unify :
-  Reduction.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
+  Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
 
 val pr_clenv : 'a clausenv -> Pp.std_ppcmds
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0256dd600..a4fb3fe9b 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -15,7 +15,7 @@ open Names
 open Term
 open Environ
 open Evd
-open Reduction
+open Reductionops
 open Typing
 open Instantiate
 open Tacred
@@ -104,7 +104,7 @@ let w_add_sign (id,t) (wc : walking_constraints) =
   ids_mk (ts_mod
             (fun evr ->
                { focus = evr.focus;
-		 hyps = Sign.add_named_assum (id,t) evr.hyps;
+		 hyps = Sign.add_named_decl (id,None,t) evr.hyps;
 		 decls = evr.decls })
             (ids_it wc))
 
@@ -144,14 +144,13 @@ let w_Declare_At sp sp' c = w_Focusing sp (w_Declare sp' c)
 
 let evars_of sigma constr = 
   let rec filtrec acc c =
-    match splay_constr c with
-    | OpEvar ev, cl ->
+    match kind_of_term c with
+    | Evar (ev, cl) ->
 	if Evd.in_dom (ts_it sigma).decls ev then
 	  Intset.add ev (Array.fold_left filtrec acc cl)
 	else
 	  Array.fold_left filtrec acc cl
-    | _, cl ->
-	Array.fold_left filtrec acc cl
+    | _ -> fold_constr filtrec acc c
   in 
   filtrec Intset.empty constr
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 58fb85240..ed13b9c25 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -13,10 +13,12 @@ open Util
 open Names
 open Evd
 open Term
+open Termops
 open Sign
 open Environ
-open Reduction
+open Reductionops
 open Inductive
+open Inductiveops
 open Typing
 open Proof_trees
 open Proof_type
@@ -31,10 +33,10 @@ open Evarutil
 variables only in Application and Case *)
 
 let collect_meta_variables c = 
-  let rec collrec acc c = match splay_constr c with
-    | OpMeta mv, _ -> mv::acc
-    | OpCast, [|c;_|] -> collrec acc c
-    | (OpApp | OpMutCase _), cl -> Array.fold_left collrec acc cl
+  let rec collrec acc c = match kind_of_term c with
+    | Meta mv -> mv::acc
+    | Cast(c,_) -> collrec acc c
+    | (App _| Case _) -> fold_constr collrec acc c
     | _ -> acc
   in 
   List.rev(collrec [] c)
@@ -64,7 +66,7 @@ let catchable_exception = function
     Nametab.GlobalizationError _)) -> true
   | _ -> false
 
-let error_cannot_unify k (m,n) =
+let error_cannot_unify (m,n) =
   raise (RefinerError (CannotUnify (m,n)))
 
 let check = ref true
@@ -91,25 +93,25 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
   else
 *)
   match kind_of_term trm with
-    | IsMeta _ ->
+    | Meta _ ->
 	if occur_meta conclty then
           raise (RefinerError (OccurMetaGoal conclty));
 	let ctxt = out_some goal.evar_info in 
 	(mk_goal ctxt hyps (nf_betaiota conclty))::goalacc, conclty
 
-    | IsCast (t,ty) ->
+    | Cast (t,ty) ->
 	let _ = type_of env sigma ty in
 	conv_leq_goal env sigma trm ty conclty;
 	mk_refgoals sigma goal goalacc ty t
 
-    | IsApp (f,l) ->
+    | App (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
 	let (acc'',conclty') =
 	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
 	let _ = conv_leq_goal env sigma trm conclty' conclty in
         (acc'',conclty')
 
-    | IsMutCase (_,p,c,lf) ->
+    | Case (_,p,c,lf) ->
 	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
@@ -132,16 +134,16 @@ and mk_hdgoals sigma goal goalacc trm =
   let env = evar_env goal in
   let hyps = goal.evar_hyps in
   match kind_of_term trm with
-    | IsCast (c,ty) when isMeta c ->
+    | Cast (c,ty) when isMeta c ->
 	let _ = type_of env sigma ty in
 	let ctxt = out_some goal.evar_info in  
 	(mk_goal ctxt hyps (nf_betaiota ty))::goalacc,ty
 
-    | IsApp (f,l) ->
+    | App (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
 	mk_arggoals sigma goal acc' hdty (Array.to_list l)
 
-    | IsMutCase (_,p,c,lf) ->
+    | Case (_,p,c,lf) ->
 	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
@@ -157,10 +159,10 @@ and mk_arggoals sigma goal goalacc funty = function
   | harg::tlargs as allargs ->
       let t = whd_betadeltaiota (evar_env goal) sigma funty in
       match kind_of_term t with
-	| IsProd (_,c1,b) ->
+	| Prod (_,c1,b) ->
 	    let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
 	    mk_arggoals sigma goal acc' (subst1 harg b) tlargs
-	| IsLetIn (_,c1,_,b) ->
+	| LetIn (_,c1,_,b) ->
 	    mk_arggoals sigma goal goalacc (subst1 c1 b) allargs
 	| _ -> raise (RefinerError (CannotApply (t,harg)))
 
@@ -170,10 +172,10 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let pj = {uj_val=p; uj_type=pt} in 
   let indspec =
-    try find_rectype env sigma ct
+    try find_mrectype env sigma ct
     with Induc -> anomaly "mk_casegoals" in
-  let (lbrty,conclty,_) =
-    type_case_branches env sigma indspec pj c in
+  let (lbrty,conclty) =
+    type_case_branches_with_names env indspec pj c in
   (acc'',lbrty,conclty)
 
 
@@ -377,15 +379,15 @@ let prim_refiner r sigma goal =
     	if !check && mem_named_context id sign then
 	  error "New variable is already declared";
         (match kind_of_term (strip_outer_cast cl) with
-	   | IsProd (_,c1,b) ->
+	   | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let sg = mk_goal info (add_named_assum (id,c1) sign)
+	       let sg = mk_goal info (add_named_decl (id,None,c1) sign)
 			  (subst1 (mkVar id) b) in
 	       [sg]
-	   | IsLetIn (_,c1,t1,b) ->
+	   | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sg =
-		 mk_goal info (add_named_def (id,c1,t1) sign)
+		 mk_goal info (add_named_decl (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
@@ -396,12 +398,12 @@ let prim_refiner r sigma goal =
     	if !check && mem_named_context id sign then
 	  error "New variable is already declared";
         (match kind_of_term (strip_outer_cast cl) with
-	   | IsProd (_,c1,b) ->
+	   | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = insert_after_hyp sign whereid (id,None,c1) in
 	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in 
 	       [sg]
-	   | IsLetIn (_,c1,t1,b) ->
+	   | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sign' = insert_after_hyp sign whereid (id,Some c1,t1) in
 	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in 
@@ -412,12 +414,12 @@ let prim_refiner r sigma goal =
 	
     | { name = Intro_replacing; newids = []; hypspecs = [id] } ->
 	(match kind_of_term (strip_outer_cast cl) with
-           | IsProd (_,c1,b) ->
+           | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,None,c1) in
 	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in
 	       [sg]
-           | IsLetIn (_,c1,t1,b) ->
+           | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,Some c1,t1) in
 	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in
@@ -432,11 +434,11 @@ let prim_refiner r sigma goal =
         let sg2 = mk_goal info (add_named_decl (id,None,t) sign) cl in
         if b then [sg1;sg2] else [sg2;sg1]  
 
-    | { name = Fix; hypspecs = []; terms = []; 
+    | { name = FixRule; hypspecs = []; terms = []; 
 	newids = [f]; params = [Num(_,n)] } ->
      	let rec check_ind k cl = 
           match kind_of_term (strip_outer_cast cl) with 
-            | IsProd (_,c1,b) -> 
+            | Prod (_,c1,b) -> 
             	if k = 1 then 
 		  try 
 		    let _ = find_inductive env sigma c1 in ()
@@ -449,13 +451,13 @@ let prim_refiner r sigma goal =
      	check_ind n cl;
 	if !check && mem_named_context f sign then
 	  error ("The name "^(string_of_id f)^" is already used");
-        let sg = mk_goal info (add_named_assum (f,cl) sign) cl in
+        let sg = mk_goal info (add_named_decl (f,None,cl) sign) cl in
         [sg]
     
-    | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
+    | { name = FixRule; hypspecs = []; terms = lar; newids = lf; params = ln } ->
      	let rec check_ind k cl = 
           match kind_of_term (strip_outer_cast cl) with 
-            | IsProd (_,c1,b) -> 
+            | Prod (_,c1,b) -> 
             	if k = 1 then 
 		  try 
 		    fst (find_inductive env sigma c1)
@@ -475,7 +477,7 @@ let prim_refiner r sigma goal =
 		       "mutual inductive declaration");
 	      if mem_named_context f sign then 
 		error "name already used in the environment";
-	      mk_sign (add_named_assum (f,ar) sign) (lar',lf',ln')
+	      mk_sign (add_named_decl (f,None,ar) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
 	      List.map (mk_goal info sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
@@ -486,7 +488,7 @@ let prim_refiner r sigma goal =
      	let rec check_is_coind cl = 
 	  let b = whd_betadeltaiota env sigma cl in
           match kind_of_term b with
-            | IsProd (_,c1,b) -> check_is_coind  b
+            | Prod (_,c1,b) -> check_is_coind  b
             | _ -> 
 		try 
 		  let _ = find_coinductive env sigma b in ()
@@ -498,10 +500,11 @@ let prim_refiner r sigma goal =
         let rec mk_sign sign = function 
           | (ar::lar'),(f::lf') ->
 	      (try
-                (let _ = lookup_id f sign in
+                (let _ = Sign.lookup_named f sign in
                 error "name already used in the environment")
               with
-              |	Not_found -> mk_sign (add_named_assum (f,ar) sign) (lar',lf'))
+              |	Not_found ->
+                  mk_sign (add_named_decl (f,None,ar) sign) (lar',lf'))
 	  | ([],[]) -> List.map (mk_goal info sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
@@ -566,10 +569,10 @@ let prim_extractor subfun vl pft =
   match pft with
     | { ref = Some (Prim { name = Intro; newids = [id] }, [spf]) } ->
 	(match kind_of_term (strip_outer_cast cl) with
-	   | IsProd (_,ty,_) ->
+	   | Prod (_,ty,_) ->
 	       let cty = subst_vars vl ty in
 	       mkLambda (Name id, cty, subfun (id::vl) spf)
-	   | IsLetIn (_,b,ty,_) ->
+	   | LetIn (_,b,ty,_) ->
 	       let cb = subst_vars vl b in
 	       let cty = subst_vars vl ty in
 	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
@@ -577,10 +580,10 @@ let prim_extractor subfun vl pft =
 	
     | { ref = Some (Prim { name = Intro_after; newids = [id]}, [spf]) } -> 
 	(match kind_of_term (strip_outer_cast cl) with
-	   | IsProd (_,ty,_) ->
+	   | Prod (_,ty,_) ->
 	       let cty = subst_vars vl ty in
 	       mkLambda (Name id, cty, subfun (id::vl) spf)
-	   | IsLetIn (_,b,ty,_) ->
+	   | LetIn (_,b,ty,_) ->
 	       let cb = subst_vars vl b in
 	       let cty = subst_vars vl ty in
 	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
@@ -588,10 +591,10 @@ let prim_extractor subfun vl pft =
 	
     | {ref=Some(Prim{name=Intro_replacing;hypspecs=[id]},[spf]) } ->
 	(match kind_of_term (strip_outer_cast cl) with
-	   | IsProd (_,ty,_) ->
+	   | Prod (_,ty,_) ->
 	       let cty = subst_vars vl ty in
 	       mkLambda (Name id, cty, subfun (id::vl) spf)
-	   | IsLetIn (_,b,ty,_) ->
+	   | LetIn (_,b,ty,_) ->
 	       let cb = subst_vars vl b in
 	       let cty = subst_vars vl ty in
 	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
@@ -601,12 +604,12 @@ let prim_extractor subfun vl pft =
         let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
 	mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2)
 
-    | {ref=Some(Prim{name=Fix;newids=[f];params=[Num(_,n)]},[spf]) } -> 
+    | {ref=Some(Prim{name=FixRule;newids=[f];params=[Num(_,n)]},[spf]) } -> 
 	let cty = subst_vars vl cl in 
 	let na = Name f in 
 	mkFix (([|n-1|],0),([|na|], [|cty|], [|subfun (f::vl) spf|]))
 
-    | {ref=Some(Prim{name=Fix;newids=lf;terms=lar;params=ln},spfl) } ->
+    | {ref=Some(Prim{name=FixRule;newids=lf;terms=lar;params=ln},spfl) } ->
 	let lcty = List.map (subst_vars vl) (cl::lar) in 
 	let vn = 
 	  Array.of_list (List.map (function Num(_,n) -> n-1
@@ -680,10 +683,10 @@ let pr_prim_rule = function
       else
         [< 'sTR"Cut "; prterm t; 'sTR ";[Intro "; pr_id id; 'sTR "|Idtac]" >]
 	
-  | {name=Fix;newids=[f];params=[Num(_,n)]} -> 
+  | {name=FixRule;newids=[f];params=[Num(_,n)]} -> 
       [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n>]
       
-  | {name=Fix;newids=(f::lf);params=(Num(_,n))::ln;terms=lar} -> 
+  | {name=FixRule;newids=(f::lf);params=(Num(_,n))::ln;terms=lar} -> 
       let rec print_mut = 
         function (f::lf),((Num(_,n))::ln),(ar::lar) -> 
           [< pr_id f; 'sTR"/"; 'iNT n; 'sTR" : "; prterm ar;
diff --git a/proofs/logic.mli b/proofs/logic.mli
index a1c525a34..3c960b657 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -61,7 +61,7 @@ type refiner_error =
 
 exception RefinerError of refiner_error
 
-val error_cannot_unify : path_kind -> constr * constr -> 'a
+val error_cannot_unify : constr * constr -> 'a
 
 val catchable_exception : exn -> bool
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 1dfc55973..5d015dbf8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -23,6 +23,7 @@ open Proof_trees
 open Proof_type
 open Lib
 open Astterm
+open Safe_typing
 
 (*********************************************************************)
 (* Managing the proofs state                                         *)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 0ea59eea2..cd63d419e 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -93,7 +93,7 @@ val suspend_proof : unit -> unit
     into a constant with its name and strength; it fails if there is
     no current proof of if it is not completed *)
 
-val cook_proof : unit -> identifier * (Declarations.constant_entry * strength)
+val cook_proof : unit -> identifier * (Safe_typing.constant_entry * strength)
 
 (*s [get_pftreestate ()] returns the current focused pending proof or
    raises [UserError "no focused proof"] *)
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 222b8277a..3003f20c6 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -12,6 +12,7 @@ open Closure
 open Util
 open Names
 open Term
+open Termops
 open Sign
 open Evd
 open Stamps
@@ -20,6 +21,7 @@ open Evarutil
 open Proof_type
 open Tacred
 open Typing
+open Nametab
 
 let is_bind = function
   | Bindings _ -> true
@@ -364,7 +366,8 @@ let last_of_cvt_flags (_,red) =
        (function
 	  | EvalVarRef id -> nvar id
 	  | EvalConstRef sp ->
-	      ast_of_qualid (Global.qualid_of_global (ConstRef sp)))
+	      ast_of_qualid
+                (qualid_of_global (Global.env()) (ConstRef sp)))
        lconst in
    if lqid = [] then []
    else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)]
@@ -384,7 +387,7 @@ let ast_of_cvt_redexp = function
       [match sp with
 	| EvalVarRef id -> nvar id
 	| EvalConstRef sp -> 					
-	    ast_of_qualid (Global.qualid_of_global (ConstRef sp))]
+	    ast_of_qualid (qualid_of_global (Global.env()) (ConstRef sp))]
       @(List.map num locc))) l)
   | Fold l ->
     ope("Fold",List.map (fun c -> ope ("COMMAND",
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index f427ec1f5..1109a5837 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -37,7 +37,7 @@ type prim_rule_name =
   | Intro_after
   | Intro_replacing
   | Cut of bool
-  | Fix
+  | FixRule
   | Cofix
   | Refine 
   | Convert_concl
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index eb31544cb..bf7162aa3 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -40,7 +40,7 @@ type prim_rule_name =
   | Intro_after
   | Intro_replacing
   | Cut of bool
-  | Fix
+  | FixRule
   | Cofix
   | Refine 
   | Convert_concl
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index e8d1574da..820c6eaff 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -12,11 +12,12 @@ open Pp
 open Util
 open Stamps
 open Term
+open Termops
 open Sign
 open Evd
 open Sign
 open Environ
-open Reduction
+open Reductionops
 open Instantiate
 open Type_errors
 open Proof_trees
@@ -52,7 +53,11 @@ let norm_goal sigma gl =
   let red_fun = Evarutil.nf_evar sigma in
   let ncl = red_fun gl.evar_concl in
   { evar_concl = ncl;
-    evar_hyps = map_named_context red_fun gl.evar_hyps;
+    evar_hyps =
+    Sign.fold_named_context 
+      (fun (d,b,ty) sign ->
+        add_named_decl (d, option_app red_fun b, red_fun ty) sign)
+      empty_named_context gl.evar_hyps;
     evar_body = gl.evar_body;
     evar_info = gl.evar_info }
 
@@ -252,7 +257,7 @@ let extract_open_proof sigma pf =
 	let abs_concl =
           List.fold_right
             (fun (_,id) concl ->
-	       let (c,ty) = lookup_id id goal.evar_hyps in
+	       let (_,c,ty) = Sign.lookup_named id goal.evar_hyps in
 	       mkNamedProd_or_LetIn (id,c,ty) concl)
             sorted_rels goal.evar_concl	in
         incr meta_cnt;
@@ -811,7 +816,7 @@ let thin_sign osign sign =
   Sign.fold_named_context
     (fun (id,c,ty as d) sign ->
        try 
-	 if lookup_id id osign = (c,ty) then sign
+	 if Sign.lookup_named id osign = (id,c,ty) then sign
 	 else raise Different
        with Not_found | Different -> add_named_decl d sign)
     sign empty_named_context
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 339a53d82..b037a4a31 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -21,6 +21,7 @@ open Sign
 open Tacred
 open Util
 open Names
+open Nameops
 open Nametab
 open Pfedit
 open Proof_type
@@ -29,7 +30,9 @@ open Tactic_debug
 open Coqast
 open Ast
 open Term
+open Termops
 open Declare
+open Safe_typing
 
 let err_msg_tactic_not_found macro_loc macro =
   user_err_loc
@@ -107,7 +110,7 @@ let make_qid = function
   | VArg (Identifier id) -> VArg (Qualid (make_short_qualid id))
   | VArg (Constr c) ->
     (match (kind_of_term c) with
-    | IsConst cst -> VArg (Qualid (qualid_of_sp cst))
+    | Const cst -> VArg (Qualid (qualid_of_sp cst))
     | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >])
   | _ -> anomalylabstrm "make_qid" [< 'sTR "Not a Qualid" >]
 
@@ -124,7 +127,7 @@ let constr_of_id id = function
     else
       let csr = global_qualified_reference (make_short_qualid id) in
       (match kind_of_term csr with
-      | IsVar _ -> raise Not_found
+      | Var _ -> raise Not_found
       | _ -> csr)
 
 (* Extracted the constr list from lfun *)
@@ -209,21 +212,21 @@ let glob_const_nvar loc env qid =
   try
     (* We first look for a variable of the current proof *)
     match Nametab.repr_qualid qid with
-      | d,id when is_empty_dirpath d ->
+      | d,id when repr_dirpath d = [] ->
 	  (* lookup_value may raise Not_found *)
-	  (match Environ.lookup_named_value id env with
-	     | Some _ ->
+	  (match Environ.lookup_named id env with
+	     | (_,Some _,_) ->
                  let v = EvalVarRef id in
                  if Opaque.is_evaluable env v then v
                  else error ("variable "^(string_of_id id)^" is opaque")
-	     | None -> error ((string_of_id id)^
+	     | _ -> error ((string_of_id id)^
 			      " does not denote an evaluable constant"))
       | _ -> raise Not_found
   with Not_found ->
   try
     let ev = (match Nametab.locate qid with
       | ConstRef sp -> EvalConstRef sp
-      | VarRef sp -> EvalVarRef (basename sp)
+      | VarRef id -> EvalVarRef id
       | _ -> error ((Nametab.string_of_qualid qid) ^
 		    " does not denote an evaluable constant")) in
     if Opaque.is_evaluable env ev then ev
@@ -1135,7 +1138,6 @@ and flag_of_ast ist lf =
         add_flag red lf
     | Node(_,"Iota",[])::lf -> add_flag (red_add red fIOTA) lf
     | Node(_,"Zeta",[])::lf -> add_flag (red_add red fZETA) lf
-    | Node(_,"Evar",[])::lf -> add_flag (red_add red fEVAR) lf
     | Node(loc,("Unf"|"UnfBut"),l)::_ ->
 	user_err_loc(loc,"flag_of_ast",
                      [<'sTR "Delta must be specified just before">])
@@ -1232,6 +1234,6 @@ let add_tacdef na vbody =
       [< 'sTR
          "There is already a Meta Definition or a Tactic Definition named ";
          pr_id na>];
-    let _ = Lib.add_leaf na OBJ (inMD (na,vbody)) in
+    let _ = Lib.add_leaf na (inMD (na,vbody)) in
     Options.if_verbose mSGNL [< pr_id na; 'sTR " is defined" >]
   end
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index d429b4069..e5ccf6d32 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -13,9 +13,10 @@ open Stamps
 open Names
 open Sign
 open Term
+open Termops
 open Instantiate
 open Environ
-open Reduction
+open Reductionops
 open Evd
 open Typing
 open Tacred
@@ -60,11 +61,13 @@ let pf_last_hyp gl = List.hd (pf_hyps gl)
 
 let pf_get_hyp gls id = 
   try 
-    lookup_id id (pf_hyps gls)
+    Sign.lookup_named id (pf_hyps gls)
   with Not_found -> 
     error ("No such hypothesis : " ^ (string_of_id id))
 
-let pf_get_hyp_typ gls id = snd (pf_get_hyp gls id)
+let pf_get_hyp_typ gls id =
+  let (_,_,ty)= (pf_get_hyp gls id) in
+  ty
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
@@ -264,7 +267,7 @@ let move_hyp with_dep id1 id2 gl =
 		  newids = []; params = []}) gl
 
 let mutual_fix lf ln lar pf = 
-  refiner (Prim { name = Fix; newids = lf;
+  refiner (Prim { name = FixRule; newids = lf;
                   hypspecs = []; terms = lar;
                   params = List.map Ast.num ln}) pf
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 640e29439..c81748a28 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -56,7 +56,7 @@ val hnf_type_of           : goal sigma -> constr -> constr
 val pf_interp_constr      : goal sigma -> Coqast.t -> constr
 val pf_interp_type        : goal sigma -> Coqast.t -> constr
 
-val pf_get_hyp            : goal sigma -> identifier -> constr option * types
+val pf_get_hyp            : goal sigma -> identifier -> named_declaration
 val pf_get_hyp_typ        : goal sigma -> identifier -> types
 
 val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr