Renommage canonique :

declaration = definition | assumption
mode de reference = named | rel

Ex:
push_named_decl : named_declaration -> env -> env
lookup_named : identifier -> safe_environment -> constr option * typed_type
add_named_assum : identifier * typed_type -> named_context -> named_context
add_named_def : identifier*constr*typed_type -> named_context -> named_context


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

15 files changed, 68 insertions, 68 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 3e55d555a6..5ef2d60357 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -33,7 +33,7 @@ type 'a clausenv = {
 type wc = walking_constraints
 
 let new_evar_in_sign env =
-  let ids = ids_of_var_context (Environ.var_context env) in
+  let ids = ids_of_named_context (Environ.named_context env) in
   let ev = new_evar () in
   mkEvar (ev, Array.of_list (List.map mkVar ids))
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 3e2d96a957..efeda72f38 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -100,7 +100,7 @@ let w_add_sign (id,t) (wc : walking_constraints) =
   ids_mk (ts_mod
             (fun evr ->
                { focus = evr.focus;
-		 env = push_var_decl (id,t) evr.env;
+		 env = push_named_assum (id,t) evr.env;
 		 decls = evr.decls })
             (ids_it wc))
 
@@ -116,7 +116,7 @@ let w_Focus sp wc = ids_mod (extract_decl sp) wc
 let w_Underlying wc = (ts_it (ids_it wc)).decls
 let w_type_of wc c  = ctxt_type_of (ids_it wc) c
 let w_env     wc    = get_env (ids_it wc)
-let w_hyps    wc    = var_context (get_env (ids_it wc))
+let w_hyps    wc    = named_context (get_env (ids_it wc))
 let w_ORELSE wt1 wt2 wc = 
   try wt1 wc with e when catchable_exception e -> wt2 wc
 
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 70416a363a..b1c4a5a2c8 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -37,9 +37,9 @@ val w_Declare    : evar -> constr * constr -> w_tactic
 val w_Declare_At : evar -> evar -> constr * constr -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
 
-val w_Underlying : walking_constraints -> evar_declarations
+val w_Underlying : walking_constraints -> enamed_declarations
 val w_env        : walking_constraints -> env
-val w_hyps       : walking_constraints -> var_context
+val w_hyps       : walking_constraints -> named_context
 val w_type_of    : walking_constraints -> constr -> constr
 val w_add_sign   : (identifier * typed_type) -> walking_constraints 
                      -> walking_constraints
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0e5b970c90..61126b262f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -223,9 +223,9 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
 let apply_to_hyp env id f =
   let found = ref false in
   let env' =
-    process_var_context_both_sides
+    process_named_context_both_sides
       (fun env (idc,c,ct as d) tail ->
-	 if idc = id then (found:=true; f env d tail) else push_var d env)
+	 if idc = id then (found:=true; f env d tail) else push_named_decl d env)
       env in
   if (not !check) || !found then env'
   else error "No such assumption"
@@ -237,7 +237,7 @@ let global_vars_set_of_var = function
 
 let check_backward_dependencies env d =
   if not (Idset.for_all
-	    (fun id -> mem_var_context id (var_context env))
+	    (fun id -> mem_named_context id (named_context env))
 	    (global_vars_set_of_var d))
   then
     error "Can't introduce at that location: free variable conflict"
@@ -255,7 +255,7 @@ let convert_hyp env sigma id ty =
     (fun env (idc,c,ct) _ ->
        if !check && not (is_conv env sigma ty (body_of_type ct)) then
 	 error "convert-hyp rule passed non-converting term";
-       push_var (idc,c,get_assumption_of env sigma ty) env)
+       push_named_decl (idc,c,get_assumption_of env sigma ty) env)
 
 let replace_hyp env id d =
   apply_to_hyp env id
@@ -263,13 +263,13 @@ let replace_hyp env id d =
        if !check then
 	 (check_backward_dependencies env d;
 	  check_forward_dependencies id tail);
-       push_var d env)
+       push_named_decl d env)
 
 let insert_after_hyp env id d =
   apply_to_hyp env id
     (fun env d' _ ->
        if !check then check_backward_dependencies env d;
-       push_var d (push_var d' env))
+       push_named_decl d (push_named_decl d' env))
 
 let remove_hyp env id =
   apply_to_hyp env id
@@ -281,33 +281,33 @@ let remove_hyp env id =
 
 let prim_refiner r sigma goal =
   let env = goal.evar_env in
-  let sign = var_context env in
+  let sign = named_context env in
   let cl = goal.evar_concl in
   let info = out_some goal.evar_info in
   match r with
     | { name = Intro; newids = [id] } ->
-    	if !check && mem_var_context id sign then
+    	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) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma c1
 	       and v = mkVar id in
-	       let sg = mk_goal info (push_var_decl (id,a) env) (subst1 v b) in
+	       let sg = mk_goal info (push_named_assum (id,a) env) (subst1 v b) in
 	       [sg]
 	   | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma t1
 	       and v = mkVar id in
 	       let sg =
-		 mk_goal info (push_var_def (id,c1,a) env) (subst1 v b) in
+		 mk_goal info (push_named_def (id,c1,a) env) (subst1 v b) in
 	       [sg]
 	   | _ ->
 	       if !check then raise (RefinerError IntroNeedsProduct)
 	       else anomaly "Intro: expects a product")
 	
     | { name = Intro_after; newids = [id]; hypspecs = [whereid] } ->
-    	if !check && mem_var_context id sign then
+    	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) ->
@@ -363,10 +363,10 @@ let prim_refiner r sigma goal =
             | _ -> error "not enough products"
 	in
      	check_ind n cl;
-	if !check && mem_var_context f sign then
+	if !check && mem_named_context f sign then
 	  error ("The name "^(string_of_id f)^" is already used");
         let a = get_assumption_of env sigma cl in
-        let sg = mk_goal info (push_var_decl (f,a) env) cl in
+        let sg = mk_goal info (push_named_assum (f,a) env) cl in
         [sg]
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
@@ -390,10 +390,10 @@ let prim_refiner r sigma goal =
 	      if not (sp=sp') then 
 		error ("fixpoints should be on the same " ^ 
 		       "mutual inductive declaration");
-	      if mem_var_context f sign then 
+	      if mem_named_context f sign then 
 		error "name already used in the environment";
 	      let a = get_assumption_of env sigma ar in
-	      mk_sign (add_var_decl (f,a) sign) (lar',lf',ln')
+	      mk_sign (add_named_assum (f,a) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
 	      List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
@@ -416,12 +416,12 @@ let prim_refiner r sigma goal =
         let rec mk_env env = function 
           | (ar::lar'),(f::lf') ->
 	      (try
-                (let _ = lookup_var f env in
+                (let _ = lookup_named f env in
                 error "name already used in the environment")
               with
               |	Not_found ->
   	        let a = get_assumption_of env sigma ar in
-	        mk_env (push_var_decl (f,a) env) (lar',lf'))
+	        mk_env (push_named_assum (f,a) env) (lar',lf'))
 	  | ([],[]) -> List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index a796cd1f44..01df402523 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -97,11 +97,11 @@ val get_pftreestate : unit -> pftreestate
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
 
-val get_goal_context : int -> evar_declarations * env
+val get_goal_context : int -> enamed_declarations * env
 
 (* [get_current_goal_context ()] works as [get_goal_context 1] *)
 
-val get_current_goal_context : unit -> evar_declarations * env
+val get_current_goal_context : unit -> enamed_declarations * env
 
 (*s [get_current_proof_name ()] return the name of the current focused
     proof or failed if no proof is focused *)
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 2f7d069a81..54febf40ba 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -76,7 +76,7 @@ let is_tactic_proof pf = (pf.subproof <> None)
    with some extra information for the program and mimick
    tactics. *)
 
-type global_constraints  = evar_declarations timestamped
+type global_constraints  = enamed_declarations timestamped
 
 (* A readable constraint is a global constraint plus a focus set
    of existential variables and a signature. *)
@@ -84,7 +84,7 @@ type global_constraints  = evar_declarations timestamped
 type evar_recordty = {
   focus : local_constraints;
   env   : env;
-  decls : evar_declarations }
+  decls : enamed_declarations }
 
 and readable_constraints = evar_recordty timestamped
 
@@ -233,7 +233,7 @@ let pr_seq evd =
     | None -> anomaly "pr_seq : info = None"
   in
   let pc = pr_ctxt info in
-  let pdcl = pr_var_context_of env in
+  let pdcl = pr_named_context_of env in
   let pcl = prterm_env_at_top env cl in
   hOV 0 [< pc; pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]
 
@@ -244,13 +244,13 @@ let prgl gl =
 
 let pr_evgl gl =
   let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
-  let phyps = pr_idl (ids_of_var_context (var_context gl.evar_env)) in
+  let phyps = pr_idl (ids_of_named_context (named_context gl.evar_env)) in
   let pc = prterm gl.evar_concl in
   hOV 0 [< 'sTR"[[" ; plc; 'sTR"] " ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
 
 let pr_evgl_sign gl = 
   let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
-  let ps = pr_var_context_of gl.evar_env in
+  let ps = pr_named_context_of gl.evar_env in
   let pc = prterm gl.evar_concl in
   hOV 0 [< 'sTR"[[" ; plc ; 'sTR"] " ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 60ae9b4f4c..56ef12fb00 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -37,7 +37,7 @@ val is_tactic_proof   : proof_tree -> bool
 (*s A global constraint is a mappings of existential variables with
     some extra information for the program and mimick tactics. *)
 
-type global_constraints = evar_declarations timestamped
+type global_constraints = enamed_declarations timestamped
 
 (*s A readable constraint is a global constraint plus a focus set
     of existential variables and a signature. *)
@@ -45,7 +45,7 @@ type global_constraints = evar_declarations timestamped
 type evar_recordty = {
   focus : local_constraints;
   env   : env;
-  decls : evar_declarations }
+  decls : enamed_declarations }
 
 and readable_constraints = evar_recordty timestamped
 
@@ -53,13 +53,13 @@ val rc_of_gc  : global_constraints -> goal -> readable_constraints
 val rc_add    : readable_constraints -> int * goal -> readable_constraints
 val get_env   : readable_constraints -> env
 val get_focus : readable_constraints -> local_constraints
-val get_decls : readable_constraints -> evar_declarations
+val get_decls : readable_constraints -> enamed_declarations
 val get_gc    : readable_constraints -> global_constraints
 val remap     : readable_constraints -> int * goal -> readable_constraints
 val ctxt_access : readable_constraints -> int -> bool
 
 val pf_lookup_name_as_renamed : 
-  var_context -> constr -> identifier -> int option
+  named_context -> constr -> identifier -> int option
 val pf_lookup_index_as_renamed : constr -> int -> int option
 
 
@@ -83,6 +83,6 @@ val pr_focus     : local_constraints -> std_ppcmds
 val pr_ctxt      : ctxtty -> std_ppcmds
 val pr_evars     : (int * goal) list -> std_ppcmds
 val pr_evars_int : int -> (int * goal) list -> std_ppcmds
-val pr_subgoals_existential : evar_declarations -> goal list -> std_ppcmds
+val pr_subgoals_existential : enamed_declarations -> goal list -> std_ppcmds
 
 val ast_of_cvt_arg : tactic_arg ->  Coqast.t 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 2a65d799b2..ac13464091 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -46,11 +46,11 @@ type ctxtty = {
   pgm    : constr option;
   lc     : local_constraints } 
 
-type evar_declarations = ctxtty evar_map
+type enamed_declarations = ctxtty evar_map
 
 (* A global constraint is a mappings of existential variables
    with some extra information for the program tactic *)
-type global_constraints  = evar_declarations timestamped
+type global_constraints  = enamed_declarations timestamped
 
 (* Signature useful to define the tactic type *)
 type 'a sigma = { 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 1b4a1c60dc..cc64be7162 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -49,11 +49,11 @@ type ctxtty = {
   pgm    : constr option;
   lc     : local_constraints } 
 
-type evar_declarations = ctxtty evar_map
+type enamed_declarations = ctxtty evar_map
 
 (* A global constraint is a mappings of existential variables
    with some extra information for the program tactic *)
-type global_constraints  = evar_declarations timestamped
+type global_constraints  = enamed_declarations timestamped
 
 (* Signature useful to define the tactic type *)
 type 'a sigma = { 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 048ce3721f..868e71f850 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -245,7 +245,7 @@ let extract_open_proof sigma pf =
             (fun id ->
                try let n = list_index id vl in (n,id)
 	       with Not_found -> failwith "caught")
-            (ids_of_var_context (evar_hyps goal)) in
+            (ids_of_named_context (evar_hyps goal)) in
 	let sorted_rels =
 	  Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
 	let abs_concl =
@@ -797,12 +797,12 @@ exception Different
 
 (* We remove from the var context of env what is already in osign *)
 let thin_sign osign env =
-  process_var_context
+  process_named_context
     (fun env (id,c,ty as d) ->
        try 
 	 if lookup_id id osign = (c,ty) then env
 	 else raise Different
-       with Not_found | Different -> push_var d env)
+       with Not_found | Different -> push_named_decl d env)
     env
 
 let rec print_proof sigma osign pf =
@@ -814,7 +814,7 @@ let rec print_proof sigma osign pf =
 	hOV 0 [< pr_seq {evar_env=env'; evar_concl=cl;
 			 evar_info=info; evar_body=body} >]
     | Some(r,spfl) ->
-  	let sign = var_context env in
+  	let sign = named_context env in
     	hOV 0 [< hOV 0 (pr_seq {evar_env=env'; evar_concl=cl;
 				evar_info=info; evar_body=body});
 		 'sPC ; 'sTR" BY ";
@@ -827,7 +827,7 @@ let pr_change gl = [< 'sTR"Change " ; prterm gl.evar_concl ; 'sTR"." ; 'fNL>]
 		     
 let rec print_script nochange sigma osign pf =
   let {evar_env=env; evar_concl=cl} = pf.goal in
-  let sign = var_context env in
+  let sign = named_context env in
   match pf.ref with
     | None ->
         if nochange then 
@@ -842,7 +842,7 @@ let rec print_script nochange sigma osign pf =
 
 let rec print_treescript sigma osign pf =
   let {evar_env=env; evar_concl=cl} = pf.goal in
-  let sign = var_context env in
+  let sign = named_context env in
   match pf.ref with
     | None -> [< >]
     | Some(r,spfl) ->
@@ -858,7 +858,7 @@ let rec print_treescript sigma osign pf =
 
 let rec print_info_script sigma osign pf =
   let {evar_env=env; evar_concl=cl} = pf.goal in
-  let sign = var_context env in
+  let sign = named_context env in
   match pf.ref with
     | None -> [< >]
     | Some(r,spfl) ->
@@ -887,7 +887,7 @@ let tclINFO (tac : tactic) gls =
   let (sgl,v) as res = tac gls in 
   begin try 
     let pf = v (List.map leaf (sig_it sgl)) in
-    let sign = var_context (sig_it gls).evar_env in
+    let sign = named_context (sig_it gls).evar_env in
     mSGNL(hOV 0 [< 'sTR" == "; 
                    print_subscript 
                      ((compose ts_it sig_sig) gls) sign pf >])
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index be59f56857..4c1e2f9770 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -104,7 +104,7 @@ type pftreestate
 val proof_of_pftreestate : pftreestate -> proof_tree
 val cursor_of_pftreestate : pftreestate -> int list
 val is_top_pftreestate : pftreestate -> bool
-val evc_of_pftreestate : pftreestate -> evar_declarations
+val evc_of_pftreestate : pftreestate -> enamed_declarations
 val top_goal_of_pftreestate : pftreestate -> goal sigma
 val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 
@@ -137,10 +137,10 @@ val change_constraints_pftreestate
 open Pp
 (*i*)
 
-val print_proof : evar_declarations -> var_context -> proof_tree -> std_ppcmds
+val print_proof : enamed_declarations -> named_context -> proof_tree -> std_ppcmds
 val pr_rule      : rule -> std_ppcmds
 val pr_tactic    : tactic_expression -> std_ppcmds
 val print_script :
-  bool -> evar_declarations -> var_context -> proof_tree -> std_ppcmds
+  bool -> enamed_declarations -> named_context -> proof_tree -> std_ppcmds
 val print_treescript :
-  evar_declarations -> var_context -> proof_tree -> std_ppcmds
+  enamed_declarations -> named_context -> proof_tree -> std_ppcmds
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index fe4ee94a47..209ea10f67 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -52,10 +52,10 @@ let constr_of_Constr_context = function
     anomalylabstrm "constr_of_Constr_context" [<'sTR
       "Not a Constr_context tactic_arg">]
 
-(* Transforms a var_context into a (string * constr) list *)
+(* Transforms a named_context into a (string * constr) list *)
 let make_hyps = List.map (fun (id,_,typ) -> (string_of_id id,body_of_type typ))
 
-(*  let lid = List.map string_of_id (ids_of_var_context hyps)
+(*  let lid = List.map string_of_id (ids_of_named_context hyps)
   and lhyp = List.map body_of_type (vals_of_sign hyps) in
     List.rev (List.combine lid lhyp)*)
 
@@ -70,7 +70,7 @@ let rec constr_list goalopt = function
        (match goalopt with
        | None -> constr_list goalopt tl
        | Some goal ->
-         if mem_var_context id (pf_hyps goal) then
+         if mem_named_context id (pf_hyps goal) then
            (id_of_string str,mkVar id)::(constr_list goalopt tl)
          else
            constr_list goalopt tl))
@@ -79,7 +79,7 @@ let rec constr_list goalopt = function
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign =
-  evar_declarations * Environ.env * (string * value) list *
+  enamed_declarations * Environ.env * (string * value) list *
     (int * constr) list * goal sigma option
 
 (* Table of interpretation functions *)
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 50b454df8f..746c89f08e 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -24,7 +24,7 @@ val constr_of_Constr : tactic_arg -> constr
 
 (* Signature for interpretation: [val_interp] and interpretation functions *)
 type interp_sign =
-  evar_declarations * Environ.env * (string * value) list * 
+  enamed_declarations * Environ.env * (string * value) list * 
     (int * constr) list * goal sigma option
 
 (* Adds a Tactic Definition in the table *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 88ca18f1c5..4b2fcbc8ef 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -37,16 +37,16 @@ let sig_it     = Refiner.sig_it
 let sig_sig    = Refiner.sig_sig
 let project    = compose ts_it sig_sig
 let pf_env gls = (sig_it gls).evar_env
-let pf_hyps gls = var_context (sig_it gls).evar_env
+let pf_hyps gls = named_context (sig_it gls).evar_env
 
 let pf_concl gls = (sig_it gls).evar_concl
 (*
 let pf_untyped_hyps gls  =
-  let sign = Environ.var_context (pf_env gls) in
+  let sign = Environ.named_context (pf_env gls) in
   map_sign_typ (fun x -> body_of_type x) sign
 *)
 let pf_hyps_types gls  =
-  let sign = Environ.var_context (pf_env gls) in
+  let sign = Environ.named_context (pf_env gls) in
   List.map (fun (id,_,x) -> (id,body_of_type x)) sign
 
 let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
@@ -59,7 +59,7 @@ let pf_get_hyp_typ gls id =
   with Not_found -> 
     error ("No such hypothesis : " ^ (string_of_id id))
 
-let pf_ids_of_hyps gls = ids_of_var_context (var_context (pf_env gls))
+let pf_ids_of_hyps gls = ids_of_named_context (named_context (pf_env gls))
 
 let pf_ctxt gls      = get_ctxt (sig_it gls)
 
@@ -278,7 +278,7 @@ let mutual_cofix lf lar pf =
     
 let rename_bound_var_goal gls =
   let { evar_env = env; evar_concl = cl } as gl = sig_it gls in 
-  let ids = ids_of_var_context (Environ.var_context env) in
+  let ids = ids_of_named_context (Environ.named_context env) in
   convert_concl (rename_bound_var ids cl) gls
     
 
@@ -510,7 +510,7 @@ open Printer
 
 let pr_com sigma goal com =
   prterm (rename_bound_var 
-            (ids_of_var_context (var_context goal.evar_env)) 
+            (ids_of_named_context (named_context goal.evar_env)) 
             (Astterm.interp_constr sigma goal.evar_env com))
 
 let pr_one_binding sigma goal = function
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 9108d48cfa..8eb0b39e6a 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -22,7 +22,7 @@ type tactic     = Proof_type.tactic;;
 
 val sig_it  : 'a sigma   -> 'a
 val sig_sig : goal sigma -> global_constraints
-val project : goal sigma -> evar_declarations
+val project : goal sigma -> enamed_declarations
 
 val re_sig : 'a -> global_constraints -> 'a sigma
 
@@ -33,11 +33,11 @@ val apply_sig_tac :
 
 val pf_concl              : goal sigma -> constr
 val pf_env                : goal sigma -> env
-val pf_hyps               : goal sigma -> var_context
+val pf_hyps               : goal sigma -> named_context
 (*i val pf_untyped_hyps       : goal sigma -> (identifier * constr) list i*)
 val pf_hyps_types         : goal sigma -> (identifier * constr) list
 val pf_nth_hyp_id         : goal sigma -> int -> identifier
-val pf_last_hyp           : goal sigma -> var_declaration
+val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> identifier list
 val pf_ctxt               : goal sigma -> ctxtty
 val pf_global             : goal sigma -> identifier -> constr
@@ -57,7 +57,7 @@ val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
 
 
 val pf_reduce : 
-  (env -> evar_declarations -> constr -> constr) ->
+  (env -> enamed_declarations -> constr -> constr) ->
     goal sigma -> constr -> constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
@@ -90,7 +90,7 @@ type pftreestate
 val proof_of_pftreestate    : pftreestate -> proof_tree
 val cursor_of_pftreestate   : pftreestate -> int list
 val is_top_pftreestate      : pftreestate -> bool
-val evc_of_pftreestate      : pftreestate -> evar_declarations
+val evc_of_pftreestate      : pftreestate -> enamed_declarations
 val top_goal_of_pftreestate : pftreestate -> goal sigma
 val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 val traverse                : int -> pftreestate -> pftreestate
@@ -193,9 +193,9 @@ val w_Focusing_THEN     : int -> 'a result_w_tactic
 val w_Declare           : int -> constr * constr -> w_tactic
 val w_Declare_At        : int -> int -> constr * constr -> w_tactic
 val w_Define            : int -> constr -> w_tactic
-val w_Underlying        : walking_constraints -> evar_declarations
+val w_Underlying        : walking_constraints -> enamed_declarations
 val w_env               : walking_constraints -> env
-val w_hyps              : walking_constraints -> var_context
+val w_hyps              : walking_constraints -> named_context
 val w_type_of           : walking_constraints -> constr -> constr
 val w_add_sign          : (identifier * typed_type) 
                           -> walking_constraints -> walking_constraints