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

12 files changed, 48 insertions, 48 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 89f84332e..c8c75cd5e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -756,7 +756,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
     List.map 
       (fun ntac -> 
 	 tclTHEN ntac
-	   (search_gen decomp (n-1) db_list local_db empty_var_context))
+	   (search_gen decomp (n-1) db_list local_db empty_named_context))
       (possible_resolve db_list local_db (pf_concl goal))
   in 
   tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
@@ -905,10 +905,10 @@ let rec super_search n db_list local_db argl goal =
 let search_superauto n ids argl g = 
   let sigma =
     List.fold_right
-      (fun id -> add_var_decl
+      (fun id -> add_named_assum
 	   (id,Retyping.get_assumption_of (pf_env g) (project g) 
 	      (pf_type_of g (pf_global g id))))
-      ids empty_var_context in
+      ids empty_named_context in
   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
   let db = Hint_db.add_list db0 (make_local_hint_db g) in
   super_search n [Stringmap.find "core" !searchtable] db argl g
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 399176c5b..14df28f54 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -88,7 +88,7 @@ val make_resolves :
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
 val make_resolve_hyp : 
-  env -> 'a evar_map -> var_declaration ->
+  env -> 'a evar_map -> named_declaration ->
       (constr_label * pri_auto_tactic) list
 
 (* [make_extern name pri pattern tactic_ast] *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 09c8767e2..8c6ace2f6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -606,7 +606,7 @@ let discr id gls =
      | Inl (cpath, (_,dirn), _) ->
 	 let e = pf_get_new_id (id_of_string "ee") gls in
 	 let e_env =
-	   push_var_decl (e,assumption_of_judgment env sigma tj) env
+	   push_named_assum (e,assumption_of_judgment env sigma tj) env
 	 in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
@@ -885,7 +885,7 @@ let inj id gls =
     | Inr posns ->
 	let e = pf_get_new_id (id_of_string "e") gls in
 	let e_env =
-	  push_var_decl (e,assumption_of_judgment env sigma tj) env
+	  push_named_assum (e,assumption_of_judgment env sigma tj) env
 	in
 	let injectors =
 	  map_succeed
@@ -951,7 +951,7 @@ let decompEqThen ntac id gls =
      | Inl (cpath, (_,dirn), _) ->
 	 let e = pf_get_new_id (id_of_string "e") gls in
 	 let e_env =
-	   push_var_decl (e,assumption_of_judgment env sigma tj) env in
+	   push_named_assum (e,assumption_of_judgment env sigma tj) env in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (pf, absurd_term) =
@@ -963,7 +963,7 @@ let decompEqThen ntac id gls =
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
 	  let e_env =
-	    push_var_decl (e,assumption_of_judgment env sigma tj) env in
+	    push_named_assum (e,assumption_of_judgment env sigma tj) env in
 	  let injectors =
 	    map_succeed
 	      (fun (cpath,t1_0,t2_0) ->
@@ -1356,7 +1356,7 @@ let sub_term_with_unif cref ceq =
 let general_rewrite_in lft2rgt id (c,lb) gls =
   let typ_id =
     (try
-       let (_,ty) = lookup_var id (pf_env gls) in (body_of_type ty)
+       let (_,ty) = lookup_named id (pf_env gls) in (body_of_type ty)
      with Not_found -> 
        errorlabstrm "general_rewrite_in" 
 	 [< 'sTR"No such hypothesis : "; print_id id >])
@@ -1422,7 +1422,7 @@ let v_conditional_rewriteRL_in =
 
 let rewrite_in lR com id gls =
   (try 
-     let _ = lookup_var id (pf_env gls) in () 
+     let _ = lookup_named id (pf_env gls) in () 
    with Not_found -> 
      errorlabstrm "rewrite_in" [< 'sTR"No such hypothesis : " ;print_id id >]);
   let c = pf_interp_constr gls com in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ed5406b79..fa2602789 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -181,7 +181,7 @@ let rec dependent_hyps id idlist sign =
   let rec dep_rec =function
     | [] -> []
     | (id1::l) -> 
-	let id1ty = snd (lookup_var id1 sign) in  
+	let id1ty = snd (lookup_named id1 sign) in  
 	if occur_var id (body_of_type id1ty) then id1::dep_rec l else dep_rec l
   in 
   dep_rec idlist 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1e115c671..9efdd718e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -94,7 +94,7 @@ let thin_ids (hyps,vars) =
 (*
 let get_local_sign sign =
   let lid = ids_of_sign sign in
-  let globsign = Global.var_context() in
+  let globsign = Global.named_context() in
   let add_local id res_sign = 
     if not (mem_sign globsign id) then 
       add_sign (lookup_sign id sign) res_sign
@@ -129,12 +129,12 @@ let rec add_prods_sign env sigma t =
 	let id = Environ.id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
 	let j = Retyping.get_assumption_of env sigma c1 in
-        add_prods_sign (Environ.push_var_decl (id,j) env) sigma b'
+        add_prods_sign (Environ.push_named_assum (id,j) env) sigma b'
     | IsLetIn (na,c1,t1,b) ->
 	let id = Environ.id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
 	let j = Retyping.get_assumption_of env sigma t1 in
-        add_prods_sign (Environ.push_var_def (id,c1,j) env) sigma b'
+        add_prods_sign (Environ.push_named_def (id,c1,j) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates wether the inversion lemma is dependent or not.
@@ -166,9 +166,9 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let i = mkAppliedInd ind in
       let ivars = global_vars i in
       let revargs,ownsign =
-	fold_var_context
+	fold_named_context
 	  (fun env (id,_,_ as d) (revargs,hyps) ->
-             if List.mem id ivars then ((mkVar id)::revargs,add_var d hyps)
+             if List.mem id ivars then ((mkVar id)::revargs,add_named_decl d hyps)
 	     else (revargs,hyps))
           env ([],[]) in
       let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
@@ -177,7 +177,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
   in
   let npty = nf_betadeltaiota env sigma pty in
   let nptyj = make_typed npty (Retyping.get_sort_of env sigma npty) in
-  let extenv = push_var_decl (p,nptyj) env in
+  let extenv = push_named_assum (p,nptyj) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
@@ -195,7 +195,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) in
   let (invEnv,invGoal) =
     compute_first_inversion_scheme env sigma ind sort dep_option in
-  assert (list_subset (global_vars invGoal) (ids_of_var_context (var_context invEnv)));
+  assert (list_subset (global_vars invGoal) (ids_of_named_context (named_context invEnv)));
 (*
     errorlabstrm "lemma_inversion"
       [< 'sTR"Computed inversion goal was not closed in initial signature" >];
@@ -205,18 +205,18 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     solve_pftreestate (tclTHEN intro 
 			 (onLastHyp (compose inv_op out_some))) pfs in
   let (pfterm,meta_types) = extract_open_pftreestate pfs in
-  let global_var_context = Global.var_context () in
+  let global_named_context = Global.named_context () in
   let ownSign =
-    fold_var_context
+    fold_named_context
       (fun env (id,_,_ as d) sign ->
-         if mem_var_context id global_var_context then sign
-	 else add_var d sign)
-      invEnv empty_var_context in
+         if mem_named_context id global_named_context then sign
+	 else add_named_decl d sign)
+      invEnv empty_named_context in
   let (_,ownSign,mvb) =
     List.fold_left
       (fun (avoid,sign,mvb) (mv,mvty) ->
          let h = next_ident_away (id_of_string "H") avoid in
-	 (h::avoid, add_var_decl (h,mvty) sign, (mv,mkVar h)::mvb))
+	 (h::avoid, add_named_assum (h,mvty) sign, (mv,mkVar h)::mvb))
       (ids_of_context invEnv, ownSign, [])
       meta_types in
   let invProof = 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 62e872184..faa49b3e2 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -120,7 +120,7 @@ let replace_in_array env a =
     
 let fresh env n =
   let id = match n with Name x -> x | _ -> id_of_string "_" in
-  next_global_ident_away id (ids_of_var_context (var_context env))
+  next_global_ident_away id (ids_of_named_context (named_context env))
 
 let rec compute_metamap env c = match kind_of_term c with
   (* le terme est directement une preuve *)
@@ -139,7 +139,7 @@ let rec compute_metamap env c = match kind_of_term c with
   | IsLambda (name,c1,c2) ->
       let v = fresh env name in
       let tj = Retyping.get_assumption_of env Evd.empty c1 in
-      let env' = push_var_decl (v,tj) env in
+      let env' = push_named_assum (v,tj) env in
       begin match compute_metamap env' (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
@@ -180,7 +180,7 @@ let rec compute_metamap env c = match kind_of_term c with
       let vi = List.rev (List.map (fresh env) fi) in
       let env' =
 	List.fold_left
-	  (fun env (v,ar) -> push_var_decl (v,Retyping.get_assumption_of env Evd.empty ar) env)
+	  (fun env (v,ar) -> push_named_assum (v,Retyping.get_assumption_of env Evd.empty ar) env)
 	  env
 	  (List.combine vi (Array.to_list ai)) 
       in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 1ed2e536b..0c513c2cf 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -65,7 +65,7 @@ let tclTRY_sign (tac : constr->tactic) sign gl =
     | [s]     -> tac (mkVar s) (*added in order to get useful error messages *)
     | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) 
   in 
-  arec (ids_of_var_context sign) gl
+  arec (ids_of_named_context sign) gl
 
 let tclTRY_HYPS (tac : constr->tactic) gl = 
   tclTRY_sign tac (pf_hyps gl) gl
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4b8993827..1f3ede393 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -34,7 +34,7 @@ val tclWEAK_PROGRESS : tactic -> tactic
 val tclNTH_HYP       : int -> (constr -> tactic) -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 val tclLAST_HYP      : (constr -> tactic) -> tactic
-val tclTRY_sign      : (constr -> tactic) -> var_context -> tactic
+val tclTRY_sign      : (constr -> tactic) -> named_context -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
 
 (*i
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index adf147b86..8264af76d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -134,7 +134,7 @@ let dyn_mutual_cofix argsl gl =
 (*          Reduction and conversion tactics                  *)
 (**************************************************************)
 
-type 'a tactic_reduction = env -> evar_declarations -> constr -> constr
+type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr
 
 (* The following two tactics apply an arbitrary
    reduction function either to the conclusion or to a 
@@ -585,7 +585,7 @@ let generalize_goal gl c cl =
 
 let generalize_dep c gl =
   let sign = pf_hyps gl in
-  let init_ids = ids_of_var_context (Global.var_context()) in
+  let init_ids = ids_of_named_context (Global.named_context()) in
   let rec seek toquant d =
     if List.exists (fun (id,_,_) -> occur_var_in_decl id d) toquant
       or dependent_in_decl c d then 
@@ -598,7 +598,7 @@ let generalize_dep c gl =
   let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
   let tothin' =
     match kind_of_term c with
-      | IsVar id when mem_var_context id sign & not (List.mem id init_ids)
+      | IsVar id when mem_named_context id sign & not (List.mem id init_ids)
 	  -> id::tothin
       | _ -> tothin
   in
@@ -669,10 +669,10 @@ let letin_abstract id c occ_ccl occ_hyps gl =
       (accu,Some hyp) 
   in
   let (depdecls,marks,rest),_ =
-    fold_var_context_reverse abstract (([],[],occ_hyps),None) env in
+    fold_named_context_reverse abstract (([],[],occ_hyps),None) env in
   if rest <> [] then begin
     let id = fst (List.hd rest) in
-    if mem_var_context id (var_context env)
+    if mem_named_context id (named_context env)
     then error ("Hypothesis "^(string_of_id id)^" occurs twice")
     else error ("No such hypothesis : " ^ (string_of_id id))
   end;
@@ -687,7 +687,7 @@ let letin_tac with_eq name c occ_ccl occ_hyps gl =
   let env = pf_env gl in
   let used_ids = ids_of_context env in
   let id = next_global_ident_away x used_ids in
-  if mem_var_context id (var_context env) then
+  if mem_named_context id (named_context env) then
     error "New variable is already declared";
   let (depdecls,marks,ccl)= letin_abstract id c occ_ccl occ_hyps gl in 
   let t = pf_type_of gl c in
@@ -1218,7 +1218,7 @@ let cook_sign hyp0 indvars env =
       else
 	Some hyp
   in
-  let _ = fold_var_context seek_deps env None in
+  let _ = fold_named_context seek_deps env None in
   (* 2nd pass from R to L: get left hyp of [hyp0] and [lhyps] *)
   let compute_lstatus lhyp (hyp,_,_ as d) =
     if hyp = hyp0 then raise (Shunt lhyp);
@@ -1229,7 +1229,7 @@ let cook_sign hyp0 indvars env =
       (Some hyp) 
   in
   try 
-    let _ = fold_var_context_reverse compute_lstatus None env in
+    let _ = fold_named_context_reverse compute_lstatus None env in
     anomaly "hyp0 not found"
   with Shunt lhyp0 ->
     let statuslists = (!lstatus,List.rev !rstatus) in
@@ -1290,7 +1290,7 @@ let get_constructors varname (elimc,elimt) mind mindpath =
 
 let induction_from_context hyp0 gl =
    (*test suivant sans doute inutile car protégé par le letin_tac avant appel*)
-  if List.mem hyp0 (ids_of_var_context (Global.var_context())) then
+  if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
     errorlabstrm "induction" [< 'sTR "Cannot generalize a global variable" >];
   let env = pf_env gl in
   let tmptyp0 = pf_get_hyp_typ gl hyp0 in
@@ -1321,7 +1321,7 @@ let induction_with_atomization_of_ind_arg hyp0 =
 
 let new_induct c gl =
   match kind_of_term c with
-    | IsVar id when not (mem_var_context id (Global.var_context())) ->
+    | IsVar id when not (mem_named_context id (Global.named_context())) ->
 	tclORELSE
 	  (tclTHEN (intros_until id) (tclLAST_HYP simplest_elim))
 	  (induction_with_atomization_of_ind_arg id) gl
@@ -1645,15 +1645,15 @@ let dyn_transitivity = function
 
 let abstract_subproof name tac gls = 
   let env = Global.env() in
-  let current_sign = Global.var_context()
+  let current_sign = Global.named_context()
   and global_sign = pf_hyps gls in
   let sign = List.fold_right
                (fun (id,_,_ as d) s -> 
-		  if mem_var_context id current_sign then s else add_var d s) 
-               global_sign empty_var_context
+		  if mem_named_context id current_sign then s else add_named_decl d s) 
+               global_sign empty_named_context
   in
   let na = next_global_ident_away name
-             (ids_of_var_context global_sign) in
+             (ids_of_named_context global_sign) in
   let concl = List.fold_left (fun t d -> mkNamedProd_or_LetIn d t)
                 (pf_concl gls) sign in
   let env' = change_hyps (fun _ -> current_sign) env in
@@ -1672,7 +1672,7 @@ let abstract_subproof name tac gls =
     Declare.construct_reference newenv CCI na
   in
   exact_no_check (applist (lemme,
-		  List.map mkVar (List.rev (ids_of_var_context sign))))
+		  List.map mkVar (List.rev (ids_of_named_context sign))))
     gls
 
 let tclABSTRACT name_op tac gls = 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e7e15881d..b41c07ec3 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -94,7 +94,7 @@ val dyn_exact_check  : tactic_arg list -> tactic
 
 (*s Reduction tactics. *)
 
-type 'a tactic_reduction = env -> evar_declarations -> constr -> constr
+type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr
 
 val reduct_in_hyp     : 'a tactic_reduction -> identifier -> tactic
 val reduct_option     : 'a tactic_reduction -> identifier option -> tactic
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 7e99167e7..6f7499057 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -1762,7 +1762,7 @@ let search env id =
   try
     mkRel (fst (lookup_rel_id id (Environ.rel_context env)))
   with Not_found ->
-  if mem_var_context id (Environ.var_context env) then
+  if mem_named_context id (Environ.named_context env) then
     mkVar id
   else
     global_reference CCI id
@@ -1851,7 +1851,7 @@ let t_exacto = ref (TVar "#")
 
 let tautoOR ti gls =
   let thyp = pf_hyps gls in
-  hipvar := ids_of_var_context thyp; 
+  hipvar := ids_of_named_context thyp; 
   let but = pf_concl gls in
   let seq = (constr_lseq gls thyp, constr_rseq gls but) in 
   let vp = lisvarprop (ante seq) in
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 320e8d56f..4943756e3 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -93,7 +93,7 @@ let clenv_constrain_with_bindings bl clause =
 let add_prod_rel sigma (t,env) =
   match kind_of_term t with
     | IsProd (na,t1,b) ->
-        (b,push_rel_decl (na,Retyping.get_assumption_of env sigma t1) env)
+        (b,push_rel_assum (na,Retyping.get_assumption_of env sigma t1) env)
     | IsLetIn (na,c1,t1,b) ->
         (b,push_rel_def (na,c1,Retyping.get_assumption_of env sigma t1) env)
     | _ -> failwith "add_prod_rel"