From bedaec8452d0600ede52efeeac016c9d323c66de Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 18 Oct 2000 14:37:44 +0000 Subject: 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 --- tactics/auto.ml | 6 +++--- tactics/auto.mli | 2 +- tactics/equality.ml | 12 ++++++------ tactics/inv.ml | 2 +- tactics/leminv.ml | 26 +++++++++++++------------- tactics/refine.ml | 6 +++--- tactics/tacticals.ml | 2 +- tactics/tacticals.mli | 2 +- tactics/tactics.ml | 30 +++++++++++++++--------------- tactics/tactics.mli | 2 +- tactics/tauto.ml | 4 ++-- tactics/wcclausenv.ml | 2 +- 12 files changed, 48 insertions(+), 48 deletions(-) (limited to 'tactics') 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" -- cgit v1.2.3