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@724 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 27 insertions, 34 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 6b45dedb0..e8aba9fe1 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -57,8 +57,8 @@ let _ = Summary.declare_summary "VARIABLE"
 
 let cache_variable (sp,((id,(d,_,_) as vd),imps)) =
   begin match d with (* Fails if not well-typed *)
-    | SectionLocalDecl ty -> Global.push_var_decl (id,ty)
-    | SectionLocalDef c -> Global.push_var_def (id,c)
+    | SectionLocalDecl ty -> Global.push_named_assum (id,ty)
+    | SectionLocalDef c -> Global.push_named_def (id,c)
   end;
   Nametab.push id sp;
   if imps then declare_var_implicits id;
@@ -204,7 +204,7 @@ let is_variable id =
   
 let out_variable sp = 
   let (id,(_,str,sticky)) = Spmap.find sp !vartab in
-  let (c,ty) = Global.lookup_var id in
+  let (c,ty) = Global.lookup_named id in
   ((id,c,ty),str,sticky)
 
 let variable_strength id =
@@ -262,7 +262,7 @@ let occur_decl env (id,c,t) hyps =
 (*
 let rec find_common_hyps_then_abstract c env hyps' = function
   | (id,_,_ as d) :: hyps when occur_decl env d hyps' ->
-      find_common_hyps_then_abstract c (Environ.push_var d env) hyps' hyps
+      find_common_hyps_then_abstract c (Environ.push_named_decl d env) hyps' hyps
   | hyps ->
       Environ.it_mkNamedLambda_or_LetIn c hyps
 
@@ -271,11 +271,11 @@ let find_common_hyps_then_abstract c env hyps' hyps =
 *)
 
 let find_common_hyps_then_abstract c env hyps' hyps = 
-  snd (fold_var_context_both_sides
+  snd (fold_named_context_both_sides
 	 (fun
 	    (env,c) (id,_,_ as d) hyps ->
 	      if occur_decl env d hyps' then 
-		(Environ.push_var d env,c)
+		(Environ.push_named_decl d env,c)
 	      else
 		(env, Environ.it_mkNamedLambda_or_LetIn c hyps))
 	 hyps
@@ -283,9 +283,9 @@ let find_common_hyps_then_abstract c env hyps' hyps =
 
 let construct_sp_reference env sp id =
   let (oper,hyps) = global_sp_operator env sp id in
-  let hyps0 = Global.var_context () in
+  let hyps0 = Global.named_context () in
   let env0 = Environ.reset_context env in
-  let args = List.map mkVar (ids_of_var_context hyps) in
+  let args = List.map mkVar (ids_of_named_context hyps) in
   let body = match oper with
     | ConstRef sp -> mkConst (sp,Array.of_list args)
     | ConstructRef sp -> mkMutConstruct (sp,Array.of_list args)
@@ -298,7 +298,7 @@ let construct_reference env kind id =
     let sp = Nametab.sp_of_id kind id in
     construct_sp_reference env sp id
   with Not_found -> 
-    mkVar (let _ = Environ.lookup_var id env in id)
+    mkVar (let _ = Environ.lookup_named id env in id)
 
 let global_sp_reference sp id = 
   construct_sp_reference (Global.env()) sp id
@@ -351,8 +351,8 @@ let elimination_suffix = function
 
 let declare_eliminations sp i =
   let mib = Global.lookup_mind sp in
-  let ids = ids_of_var_context mib.mind_hyps in
-  if not (list_subset ids (ids_of_var_context (Global.var_context ()))) then
+  let ids = ids_of_named_context mib.mind_hyps in
+  if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then
     error ("Declarations of elimination scheme outside the section "^
     "of the inductive definition is not implemented");
   let ctxt = Array.of_list (List.map mkVar ids) in
diff --git a/library/declare.mli b/library/declare.mli
index 4a33500fc..cd931d94d 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -50,7 +50,7 @@ val constant_strength : section_path -> strength
 val constant_or_parameter_strength : section_path -> strength
 
 val is_variable : identifier -> bool
-val out_variable : section_path -> var_declaration * strength * sticky
+val out_variable : section_path -> named_declaration * strength * sticky
 val variable_strength : identifier -> strength
 
 
@@ -58,7 +58,7 @@ val variable_strength : identifier -> strength
     construtor) corresponding to [id] in global environment, together
     with its definition environment. *)
 
-val global_operator : path_kind -> identifier -> global_reference * var_context
+val global_operator : path_kind -> identifier -> global_reference * named_context
 
 (*s [global_reference k id] returns the object corresponding to
     the name [id] in the global environment. It may be a constant, 
diff --git a/library/global.ml b/library/global.ml
index 96fb689a3..52ea32986 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -28,22 +28,19 @@ let _ =
 
 let universes () = universes !global_env
 let context () = context !global_env
-let var_context () = var_context !global_env
+let named_context () = named_context !global_env
+
+let push_named_def idc = global_env := push_named_def idc !global_env
+let push_named_assum idc = global_env := push_named_assum idc !global_env
 
-let push_var_def idc = global_env := push_var_def idc !global_env
-let push_var_decl idc = global_env := push_var_decl idc !global_env
-(*
-let push_rel_def nac = global_env := push_rel nac !global_env
-let push_rel_decl nac = global_env := push_rel nac !global_env
-*)
 let add_constant sp ce = global_env := add_constant sp ce !global_env
 let add_parameter sp c = global_env := add_parameter sp c !global_env
 let add_mind sp mie = global_env := add_mind sp mie !global_env
 let add_constraints c = global_env := add_constraints c !global_env
 
-let pop_vars ids = global_env := pop_vars ids !global_env
+let pop_named_decls ids = global_env := pop_named_decls ids !global_env
 
-let lookup_var id = lookup_var id !global_env
+let lookup_named id = lookup_named id !global_env
 (*
 let lookup_rel n = lookup_rel n !global_env
 *)
diff --git a/library/global.mli b/library/global.mli
index 16ed53785..88f690c54 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -21,23 +21,19 @@ val env : unit -> env
 
 val universes : unit -> universes
 val context : unit -> context
-val var_context : unit -> var_context
-
-val push_var_decl : identifier * constr -> unit
-val push_var_def : identifier * constr -> unit
-(*i
-val push_var : identifier * constr option * constr -> unit
-val push_rel_decl : name * constr -> unit
-val push_rel_def : name * constr -> unit
-i*)
+val named_context : unit -> named_context
+
+val push_named_assum : identifier * constr -> unit
+val push_named_def : identifier * constr -> unit
+
 val add_constant : section_path -> constant_entry -> unit
 val add_parameter : section_path -> constr -> unit
 val add_mind : section_path -> mutual_inductive_entry -> unit
 val add_constraints : constraints -> unit
 
-val pop_vars : identifier list -> unit
+val pop_named_decls : identifier list -> unit
 
-val lookup_var : identifier -> constr option * typed_type
+val lookup_named : identifier -> constr option * typed_type
 (*i val lookup_rel : int -> name * typed_type i*)
 val lookup_constant : section_path -> constant_body
 val lookup_mind : section_path -> mutual_inductive_body
diff --git a/library/impargs.ml b/library/impargs.ml
index e2cd81f4e..17cd54b2c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -100,7 +100,7 @@ let var_table = ref Idmap.empty
 
 let declare_var_implicits id =
   let env = Global.env () in
-  let (_,ty) = lookup_var id env in
+  let (_,ty) = lookup_named id env in
   let imps = auto_implicits env (body_of_type ty) in
   var_table := Idmap.add id imps !var_table