aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/termops.ml7
-rw-r--r--engine/termops.mli2
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/pre_env.ml3
-rw-r--r--kernel/pre_env.mli1
-rw-r--r--pretyping/unification.ml2
-rw-r--r--proofs/logic.ml2
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/tactics.ml24
11 files changed, 27 insertions, 26 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index a047bf53c..17e56ec31 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -975,11 +975,8 @@ let smash_rel_context sign =
let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
-let rec mem_named_context id ctxt =
- match ctxt with
- | decl :: _ when Id.equal id (NamedDecl.get_id decl) -> true
- | _ :: sign -> mem_named_context id sign
- | [] -> false
+let mem_named_context_val id ctxt =
+ try Environ.lookup_named_val id ctxt; true with Not_found -> false
let compact_named_context_reverse sign =
let compact l decl =
diff --git a/engine/termops.mli b/engine/termops.mli
index 5d85088f8..0a7ac1f26 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -237,7 +237,7 @@ val map_rel_context_with_binders :
val fold_named_context_both_sides :
('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
Context.Named.t -> init:'a -> 'a
-val mem_named_context : Id.t -> Context.Named.t -> bool
+val mem_named_context_val : Id.t -> named_context_val -> bool
val compact_named_context : Context.Named.t -> Context.NamedList.t
val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 96e35610c..54898320d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -116,7 +116,7 @@ let val_of_named_context ctxt =
List.fold_right push_named_context_val ctxt empty_named_context_val
-let lookup_named id env = fst (Id.Map.find id env.env_named_context.env_named_map)
+let lookup_named = lookup_named
let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map)
let eq_named_context_val c1 c2 =
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 79930f6ad..bf40f7389 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1845,7 +1845,7 @@ and compile_rel env sigma univ auxdefs n =
and compile_named env sigma univ auxdefs id =
let open Context.Named.Declaration in
- match Context.Named.lookup id env.env_named_context.env_named_ctx with
+ match lookup_named id env with
| LocalDef (_,t,_) ->
let code = lambda_of_constr env sigma t in
let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 104fe59d1..7be8606ef 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -173,6 +173,9 @@ let push_named d env =
indirect_pterms = env.indirect_pterms;
}
+let lookup_named id env =
+ fst (Id.Map.find id env.env_named_context.env_named_map)
+
let lookup_named_val id env =
snd(Id.Map.find id env.env_named_context.env_named_map)
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 1e4eff3d5..866790367 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -81,6 +81,7 @@ val map_named_val :
(constr -> constr) -> named_context_val -> named_context_val
val push_named : Context.Named.Declaration.t -> env -> env
+val lookup_named : Id.t -> env -> Context.Named.Declaration.t
val lookup_named_val : Id.t -> env -> lazy_val
val env_of_named : Id.t -> env -> env
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6d80db645..36353653a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1586,7 +1586,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let x = id_of_name_using_hdchar (Global.env()) t name in
let ids = ids_of_named_context (named_context env) in
if name == Anonymous then next_ident_away_in_goal x ids else
- if mem_named_context x (named_context env) then
+ if mem_named_context_val x (named_context_val env) then
errorlabstrm "Unification.make_abstraction_core"
(str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
else
diff --git a/proofs/logic.ml b/proofs/logic.ml
index aa0b9bac6..cc95de646 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -533,7 +533,7 @@ let prim_refiner r sigma goal =
nexthyp,
t,cl,sigma
else
- (if !check && mem_named_context id (named_context_of_val sign) then
+ (if !check && mem_named_context_val id sign then
errorlabstrm "Logic.prim_refiner"
(str "Variable " ++ pr_id id ++ str " is already declared.");
push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 50984c48e..ba22db083 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -191,9 +191,9 @@ module New = struct
next_ident_away id ids
let pf_get_hyp id gl =
- let hyps = Proofview.Goal.hyps gl in
+ let hyps = Proofview.Goal.env gl in
let sign =
- try Context.Named.lookup id hyps
+ try Environ.lookup_named id hyps
with Not_found -> raise (RefinerError (NoSuchHyp id))
in
sign
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 642bf520b..40b600c89 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -202,11 +202,11 @@ let inversion_scheme env sigma t sort dep_option inv_op =
tclTHEN intro (onLastHypId inv_op)) pf)
in
let pfterm = List.hd (Proof.partial_proof pf) in
- let global_named_context = Global.named_context () in
+ let global_named_context = Global.named_context_val () in
let ownSign = ref begin
fold_named_context
(fun env d sign ->
- if mem_named_context (get_id d) global_named_context then sign
+ if mem_named_context_val (get_id d) global_named_context then sign
else Context.Named.add d sign)
invEnv ~init:Context.Named.empty
end in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f47141efb..e93a82e4d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -179,10 +179,10 @@ let introduction ?(check=true) id =
let gl = Proofview.Goal.assume gl in
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
- let hyps = Proofview.Goal.hyps gl in
+ let hyps = named_context_val (Proofview.Goal.env gl) in
let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
- let () = if check && mem_named_context id hyps then
+ let () = if check && mem_named_context_val id hyps then
errorlabstrm "Tactics.introduction"
(str "Variable " ++ pr_id id ++ str " is already declared.")
in
@@ -507,7 +507,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
let (sp', u') = check_mutind env sigma n ar in
if not (eq_mind sp sp') then
error "Fixpoints should be on the same mutual inductive declaration.";
- if mem_named_context f (named_context_of_val sign) then
+ if mem_named_context_val f sign then
errorlabstrm "Logic.prim_refiner"
(str "Name " ++ pr_id f ++ str " already used in the environment");
mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
@@ -560,7 +560,7 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
| [] -> sign
| (f, ar) :: oth ->
let open Context.Named.Declaration in
- if mem_named_context f (named_context_of_val sign) then
+ if mem_named_context_val f sign then
error "Name already used in the environment.";
mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
in
@@ -2782,7 +2782,7 @@ let old_generalize_dep ?(with_let=false) c gl =
let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
let tothin' =
match kind_of_term c with
- | Var id when mem_named_context id sign && not (Id.List.mem id init_ids)
+ | Var id when mem_named_context_val id (val_of_named_context sign) && not (Id.List.mem id init_ids)
-> id::tothin
| _ -> tothin
in
@@ -2932,8 +2932,8 @@ let unfold_body x =
let open Context.Named.Declaration in
Proofview.Goal.enter { enter = begin fun gl ->
(** We normalize the given hypothesis immediately. *)
- let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
- let xval = match Context.Named.lookup x hyps with
+ let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
+ let xval = match Environ.lookup_named x env with
| LocalAssum _ -> errorlabstrm "unfold_body"
(pr_id x ++ str" is not a defined hypothesis.")
| LocalDef (_,xval,_) -> xval
@@ -4355,7 +4355,7 @@ let induction_gen clear_flag isrec with_evars elim
let cls = Option.default allHypsAndConcl cls in
let t = typ_of env sigma c in
let is_arg_pure_hyp =
- isVar c && not (mem_named_context (destVar c) (Global.named_context()))
+ isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ()))
&& lbind == NoBindings && not with_evars && Option.is_empty eqname
&& clear_flag == None
&& has_generic_occurrences_but_goal cls (destVar c) env ccl in
@@ -4402,7 +4402,7 @@ let induction_gen_l isrec with_evars elim names lc =
| [] -> Proofview.tclUNIT ()
| c::l' ->
match kind_of_term c with
- | Var id when not (mem_named_context id (Global.named_context()))
+ | Var id when not (mem_named_context_val id (Global.named_context_val ()))
&& not with_evars ->
let _ = newlc:= id::!newlc in
atomize_list l'
@@ -4824,7 +4824,7 @@ let abstract_subproof id gk tac =
let open Context.Named.Declaration in
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
- let current_sign = Global.named_context()
+ let current_sign = Global.named_context_val ()
and global_sign = Proofview.Goal.hyps gl in
let sigma = Sigma.to_evar_map sigma in
let evdref = ref sigma in
@@ -4832,8 +4832,8 @@ let abstract_subproof id gk tac =
List.fold_right
(fun d (s1,s2) ->
let id = get_id d in
- if mem_named_context id current_sign &&
- interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d
+ if mem_named_context_val id current_sign &&
+ interpretable_as_section_decl evdref (lookup_named_val id current_sign) d
then (s1,push_named_context_val d s2)
else (Context.Named.add d s1,s2))
global_sign (Context.Named.empty, empty_named_context_val) in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 16:25:52 +0000