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

4 files changed, 23 insertions, 23 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 5e6137db01..bdf48ddbb5 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -253,7 +253,7 @@ let error_fixname_unbound str is_cofix loc name =
 	  'sTR ((if is_cofix then "co" else "")^"fixpoint definition") >])
 (*
 let rec collapse_env n env = if n=0 then env else
-  add_rel (Anonymous,()) (collapse_env (n-1) (snd (uncons_rel_env env)))
+  add_rel_decl (Anonymous,()) (collapse_env (n-1) (snd (uncons_rel_env env)))
 *)
 
 let check_capture s ty = function
@@ -459,8 +459,8 @@ let ast_adjust_consts sigma =
   dbrec
 
 let globalize_constr ast =
-  let sign = Global.var_context () in
-  ast_adjust_consts Evd.empty (from_list (ids_of_var_context sign)) ast
+  let sign = Global.named_context () in
+  ast_adjust_consts Evd.empty (from_list (ids_of_named_context sign)) ast
 
 (* Globalizes ast expressing constructions in tactics or vernac *)
 (* Actually, it is incomplete, see vernacinterp.ml and tacinterp.ml *)
@@ -479,8 +479,8 @@ let rec glob_ast sigma env =
   | x -> x
 
 let globalize_ast ast =
-  let sign = Global.var_context () in
-  glob_ast Evd.empty (from_list (ids_of_var_context sign)) ast
+  let sign = Global.named_context () in
+  glob_ast Evd.empty (from_list (ids_of_named_context sign)) ast
 
 (**************************************************************************)
 (* Functions to translate ast into rawconstr                              *)
@@ -489,7 +489,7 @@ let globalize_ast ast =
 let interp_rawconstr_gen sigma env allow_soapp lvar com =
   ast_to_rawconstr sigma
     (from_list (ids_of_rel_context (rel_context env)))
-    allow_soapp (lvar,var_context env) com
+    allow_soapp (lvar,named_context env) com
 
 let interp_rawconstr sigma env com =
   interp_rawconstr_gen sigma env false [] com
@@ -500,7 +500,7 @@ let interp_rawconstr sigma env com =
 let interp_rawconstr_wo_glob sigma env lvar com =
   ast_to_rawconstr sigma
     (from_list (ids_of_rel_context (rel_context env)))
-    false (lvar,var_context env) com
+    false (lvar,named_context env) com
 
 (*let raw_fconstr_of_com sigma env com =
   ast_to_fw sigma (unitize_env (context env)) [] com
@@ -619,7 +619,7 @@ let interp_constrpattern_gen sigma env lvar com =
     ast_to_rawconstr sigma (from_list (ids_of_rel_context (rel_context env)))
       true (List.map
 	      (fun x ->
-		 string_of_id (fst x)) lvar,var_context env) com
+		 string_of_id (fst x)) lvar,named_context env) com
   and nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in
   try 
     pattern_of_rawconstr nlvar c
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 1e81bf2844..43f28fbe6b 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -115,8 +115,8 @@ let implicit_args_msg sp mipv =
           >])
        mipv >]
 
-let instance_of_var_context sign =
-  Array.of_list (List.map mkVar (ids_of_var_context sign))
+let instance_of_named_context sign =
+  Array.of_list (List.map mkVar (ids_of_named_context sign))
 
 let print_mutual sp mib = 
   let pk = kind_of_path sp in
@@ -147,7 +147,7 @@ let print_mutual sp mib =
     else
       [< 'sTR "["; pr_rel_context env lpars; 'sTR "]"; 'bRK(1,2) >] in
   let print_oneind tyi =
-    let mis = build_mis ((sp,tyi),instance_of_var_context mib.mind_hyps) mib in
+    let mis = build_mis ((sp,tyi),instance_of_named_context mib.mind_hyps) mib in
     let (_,arity) = decomp_n_prod env evd nparams
 		      (body_of_type (mis_user_arity mis)) in
       (hOV 0
@@ -156,7 +156,7 @@ let print_mutual sp mib =
 	          'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]);
             'bRK(1,2); print_constructors mis >]) 
   in 
-  let mis0 = build_mis ((sp,0),instance_of_var_context mib.mind_hyps) mib in
+  let mis0 = build_mis ((sp,0),instance_of_named_context mib.mind_hyps) mib in
   (* Case one [co]inductive *)
   if Array.length mipv = 1 then
     let (_,arity) = decomp_n_prod env evd nparams
@@ -431,7 +431,7 @@ let print_name name =
       | ConstructRef ((sp,_),_) -> print_inductive sp
   with Not_found -> 
   try
-    let (c,typ) = Global.lookup_var name in 
+    let (c,typ) = Global.lookup_named name in 
     [< print_var (name,c,typ);
        try print_impl_args (implicits_of_var name)
        with _ -> [<>] >]
@@ -440,7 +440,7 @@ let print_name name =
 let print_opaque_name name = 
   let sigma = Evd.empty in
   let env = Global.env () in
-  let sign = Global.var_context () in
+  let sign = Global.named_context () in
   try 
     let x = global_reference CCI name in
     match kind_of_term x with
@@ -457,7 +457,7 @@ let print_opaque_name name =
 	  let ty = Typeops.type_of_constructor env sigma cstr in
 	  print_typed_value (x, ty)
       | IsVar id ->
-          let (c,ty) = lookup_var id env in 
+          let (c,ty) = lookup_named id env in 
 	  print_var (id,c,ty)
       | _ -> failwith "print_name"
   with Not_found -> 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index e8eccf6834..04578675ac 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -186,8 +186,8 @@ let pr_rel_decl env (na,c,typ) =
  * It's printed out from outermost to innermost, so it's readable. *)
 
 (* Prints a signature, all declarations on the same line if possible *)
-let pr_var_context_of env =
-  hV 0 [< (fold_var_context
+let pr_named_context_of env =
+  hV 0 [< (fold_named_context
 	     (fun env d pps -> [< pps; 'wS 2; pr_var_decl env d >])
              env) [< >] >]
 
@@ -205,7 +205,7 @@ let pr_rel_context env rel_context =
 (* Prints an env (variables and de Bruijn). Separator: newline *)
 let pr_context_unlimited env =
   let sign_env =
-    fold_var_context
+    fold_named_context
       (fun env d pps ->
          let pidt =  pr_var_decl env d in [< pps; 'fNL; pidt >])
       env [< >] 
@@ -223,14 +223,14 @@ let pr_ne_context_of header k env =
   else let penv = pr_context_unlimited env in [< header; penv >]
 
 let pr_context_limit n env =
-  let var_context = Environ.var_context env in
-  let lgsign = List.length var_context in
+  let named_context = Environ.named_context env in
+  let lgsign = List.length named_context in
   if n >= lgsign then 
     pr_context_unlimited env
   else
     let k = lgsign-n in
     let _,sign_env =
-      fold_var_context
+      fold_named_context
         (fun env d (i,pps) ->
            if i < k then 
 	     (i+1, [< pps ;'sTR "." >])
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 67434ee317..3e5b589b4a 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -36,10 +36,10 @@ val pr_pattern_env  : names_context -> constr_pattern -> std_ppcmds
 
 val pr_ne_context_of : std_ppcmds -> path_kind -> env -> std_ppcmds
 
-val pr_var_decl     : env -> var_declaration -> std_ppcmds
+val pr_var_decl     : env -> named_declaration -> std_ppcmds
 val pr_rel_decl     : env -> rel_declaration -> std_ppcmds
 
-val pr_var_context_of : env -> std_ppcmds
+val pr_named_context_of : env -> std_ppcmds
 val pr_rel_context  : env -> rel_context -> std_ppcmds
 val pr_context_of   : env -> std_ppcmds