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

8 files changed, 24 insertions, 24 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1fd4fc4034..6150f0c024 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -141,7 +141,7 @@ let build_mutual lparams lnamearconstrs finite =
            let raw_arity = mkProdCit lparams arityc in
            let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
 	   let arity = Typeops.assumption_of_type_judgment arj in
-	   let env' = Environ.push_rel_decl (Name recname,arity) env in
+	   let env' = Environ.push_rel_assum (Name recname,arity) env in
 	   (env', (arity::arl)))
 	(env0,[]) lnamearconstrs 
     in
@@ -218,7 +218,7 @@ let build_recursive lnameargsardef =
 	   let arity = Typeops.assumption_of_type_judgment arj in
            declare_variable recname
 	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
-           (Environ.push_var_decl (recname,arity) env, (arity::arl)))
+           (Environ.push_named_assum (recname,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
     with e ->
       States.unfreeze fs; raise e
@@ -286,7 +286,7 @@ let build_corecursive lnameardef =
 	   let arity = Typeops.assumption_of_type_judgment arj in
            declare_variable recname
 	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
-           (Environ.push_var_decl (recname,arity) env, (arity::arl)))
+           (Environ.push_named_assum (recname,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
       States.unfreeze fs; raise e
diff --git a/toplevel/command.mli b/toplevel/command.mli
index fb9071d0f7..263d670324 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -56,4 +56,4 @@ theorem under the name [name] and gives it the strength of a remark *)
 
 val save_anonymous_remark : bool -> string -> unit
 
-val get_current_context : unit -> Proof_type.evar_declarations * Environ.env
+val get_current_context : unit -> Proof_type.enamed_declarations * Environ.env
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 17ccac01d5..2cfd2ca647 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -236,7 +236,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
 	    (Array.map (expmod_type oldenv modlist) (mind_user_lc mip))))
       mib.mind_packets
   in
-  let hyps' = map_var_context (expmod_constr oldenv modlist) mib.mind_hyps in
+  let hyps' = map_named_context (expmod_constr oldenv modlist) mib.mind_hyps in
   let (inds',modl) = abstract_inductive ids_to_discard hyps' inds in
   let lmodif_one_mind i = 
     let nbc = Array.length (mind_nth_type_packet mib i).mind_consnames in 
@@ -261,7 +261,7 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
   let body = 
     expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in
   let typ = expmod_type oldenv modlist cb.const_type in
-  let hyps = map_var_context (expmod_constr oldenv modlist) cb.const_hyps in
+  let hyps = map_named_context (expmod_constr oldenv modlist) cb.const_hyps in
   let (body',typ',modl) = abstract_constant ids_to_discard hyps (body,typ) in
   let mods = [ (ConstRef osecsp, DO_ABSTRACT(ConstRef nsecsp,modl)) ] in
   (body', body_of_type typ', mods)
@@ -403,7 +403,7 @@ let close_section _ s =
   let (sec_sp,decls) = close_section s in
   let (ops,ids,_) = 
     List.fold_left (process_item oldenv sec_sp) ([],[],[]) decls in 
-  Global.pop_vars ids;
+  Global.pop_named_decls ids;
   List.iter process_operation (List.rev ops)
 
 
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index 92fb1bd93b..aecec0c251 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -30,19 +30,19 @@ module Make = functor (P : Printer) -> struct
 
 (****
   let sign_it_with f sign e =
-    snd (fold_var_context
-	   (fun (id,v,t) (sign,e) -> (add_var (id,v,t) sign, f id t sign e))
-           sign (empty_var_context,e))
+    snd (fold_named_context
+	   (fun (id,v,t) (sign,e) -> (add_named_decl (id,v,t) sign, f id t sign e))
+           sign (empty_named_context,e))
 
   let dbenv_it_with f env e =
     snd (dbenv_it 
-	   (fun na t (env,e) -> (add_rel (na,t) env, f na t env e))
+	   (fun na t (env,e) -> (add_rel_decl (na,t) env, f na t env e))
            env (gLOB(get_globals env),e))
 ****)
       
   let pr_env k env =
     let sign_env =
-      fold_var_context
+      fold_named_context
 	(fun env (id,_,t) pps ->
            let pidt =  print_decl k env (id,t) in [<  pps ; 'fNL ; pidt >])
 	env [< >] 
@@ -56,7 +56,7 @@ module Make = functor (P : Printer) -> struct
     [< sign_env; db_env >]
     
   let pr_ne_ctx header k env =
-    if rel_context env = [] && var_context env = [] then
+    if rel_context env = [] && named_context env = [] then
       [< >]
     else
       [< header; pr_env k env >]
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b7bd4ecfe4..1fe9d21aba 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -95,7 +95,7 @@ let explain_generalization k ctx (name,var) j =
   let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of [< 'sTR"in environment" >] k ctx in
   let pv = prtype_env ctx var in
-  let (pc,pt) = prjudge_env (push_rel_decl (name,var) ctx) j in
+  let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in
   [< 'sTR"Illegal generalization: "; pe; 'fNL;
      'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
      'sTR"over"; 'bRK(1,1); pc; 'sTR","; 'sPC; 'sTR"it has type"; 'sPC; pt; 
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 171f31dae4..6276438e10 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -15,7 +15,7 @@ open G_minicoq
 
 let (env : safe_environment ref) = ref empty_environment
 
-let lookup_var id =
+let lookup_named id =
   let rec look n = function
     | [] -> mkVar id
     | (Name id')::_ when id = id' -> Rel n
@@ -23,10 +23,10 @@ let lookup_var id =
   in
   look 1
 
-let args sign = Array.of_list (List.map mkVar (ids_of_var_context sign))
+let args sign = Array.of_list (List.map mkVar (ids_of_named_context sign))
 
 let rec globalize bv c = match kind_of_term c with
-  | IsVar id -> lookup_var id bv
+  | IsVar id -> lookup_named id bv
   | IsConst (sp, _) ->
       let cb = lookup_constant sp !env in mkConst (sp, args cb.const_hyps)
   | IsMutInd (sp,_ as spi, _) ->
@@ -59,7 +59,7 @@ let parameter id t =
 
 let variable id t =
   let t = globalize [] t in
-  env := push_var_decl (id,t) !env;
+  env := push_named_assum (id,t) !env;
   mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; print_id id; 
 		  'sPC; 'sTR"is declared"; 'fNL >])
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f23430ae4b..321f9bf31b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -73,7 +73,7 @@ let typecheck_params_and_field ps fs =
       (fun (env,newps) (id,t) -> 
          let tj = type_judgment_of_rawconstr Evd.empty env t in
 	 let ass = Typeops.assumption_of_type_judgment tj in
-         (Environ.push_var_decl (id,ass) env,(id,tj.Environ.utj_val)::newps))
+         (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newps))
       (env0,[]) ps
   in
   let env2,newfs =
@@ -81,7 +81,7 @@ let typecheck_params_and_field ps fs =
       (fun (env,newfs) (id,t) -> 
          let tj = type_judgment_of_rawconstr Evd.empty env t in
 	 let ass = Typeops.assumption_of_type_judgment tj in
-         (Environ.push_var_decl (id,ass) env,(id,tj.Environ.utj_val)::newfs)) (env1,[]) fs
+         (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newfs)) (env1,[]) fs
   in
   List.rev(newps),List.rev(newfs)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a1db3b78a1..afe871641e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -48,13 +48,13 @@ let show_script () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  mSGNL(Refiner.print_script true evc (Global.var_context()) pf)
+  mSGNL(Refiner.print_script true evc (Global.named_context()) pf)
 
 let show_prooftree () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  mSG(Refiner.print_proof evc (Global.var_context()) pf)
+  mSG(Refiner.print_proof evc (Global.named_context()) pf)
 
 let show_open_subgoals () =
   let pfts = get_pftreestate () in
@@ -591,7 +591,7 @@ let _ =
            | (n::l) -> aux (Tacmach.traverse n pts) l in 
          let pts = aux pts (l@[-1]) in
          let pf = proof_of_pftreestate pts in 
-	 mSG (Refiner.print_script true evc (Global.var_context()) pf))
+	 mSG (Refiner.print_script true evc (Global.named_context()) pf))
 
 let _ =
   add "ExplainProofTree"
@@ -608,7 +608,7 @@ let _ =
            | (n::l) -> aux (Tacmach.traverse n pts) l in 
          let pts = aux pts (l@[-1]) in
          let pf = proof_of_pftreestate pts in 
-	 mSG (Refiner.print_proof evc (Global.var_context()) pf))
+	 mSG (Refiner.print_proof evc (Global.named_context()) pf))
 
 let _ =
   add "ShowProofs"