diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 5 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 | ||||
| -rw-r--r-- | kernel/evd.ml | 2 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 6 | ||||
| -rw-r--r-- | kernel/safe_typing.ml (renamed from kernel/typing.ml) | 5 | ||||
| -rw-r--r-- | kernel/safe_typing.mli (renamed from kernel/typing.mli) | 1 | ||||
| -rw-r--r-- | kernel/sign.ml | 6 | ||||
| -rw-r--r-- | kernel/sign.mli | 44 | ||||
| -rw-r--r-- | kernel/typeops.ml | 6 |
10 files changed, 41 insertions, 37 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index ccf3e1e20c..bed45797d8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -43,6 +43,7 @@ let empty_env = { let universes env = env.env_universes let context env = env.env_context +let var_context env = let (ENVIRON(g,_)) = env.env_context in g (* Construction functions. *) @@ -50,8 +51,8 @@ let push_var idvar env = { env with env_context = add_glob idvar env.env_context } let change_hyps f env = - let ctx = env.env_context in - { env with env_context = ENVIRON (f (get_globals ctx), get_rels ctx) } + let (ENVIRON(g,r)) = env.env_context in + { env with env_context = ENVIRON (f g, r) } let push_rel idrel env = { env with env_context = add_rel idrel env.env_context } diff --git a/kernel/environ.mli b/kernel/environ.mli index d3fd22c01e..9f1c228a00 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -22,6 +22,7 @@ val empty_env : unsafe_env val universes : unsafe_env -> universes val context : unsafe_env -> context +val var_context : unsafe_env -> var_context val push_var : identifier * typed_type -> unsafe_env -> unsafe_env val change_hyps : diff --git a/kernel/evd.ml b/kernel/evd.ml index dd387ddfb4..4599fbdc43 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -65,7 +65,7 @@ let is_defined sigma ev = let info = map sigma ev in not (info.evar_body = Evar_empty) -let evar_hyps ev = get_globals (context ev.evar_env) +let evar_hyps ev = var_context ev.evar_env let id_of_existential ev = id_of_string ("?" ^ string_of_int ev) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 96fe8d5846..00e8a442bb 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -244,7 +244,7 @@ let cci_inductive env env_ar kind nparams finite inds cst = let packets = Array.of_list (list_map_i one_packet 1 inds) in { mind_kind = kind; mind_ntypes = ntypes; - mind_hyps = get_globals (context env); + mind_hyps = var_context env; mind_packets = packets; mind_constraints = cst; mind_singl = None; diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4bc551c6aa..2ce121ed12 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1296,17 +1296,17 @@ let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables * Similarly we have is_fmachine1_metas and is_resolve1_metas *) -let rec whd_ise1_metas env sigma = function +let rec whd_ise1_metas sigma = function | (DOPN(Evar n,_) as k) -> if Evd.in_dom sigma n then if Evd.is_defined sigma n then - whd_ise1_metas env sigma (existential_value sigma k) + whd_ise1_metas sigma (existential_value sigma k) else let m = DOP0(Meta (new_meta())) in DOP2(Cast,m,existential_type sigma k) else k - | DOP2(Cast,c,_) -> whd_ise1_metas env sigma c + | DOP2(Cast,c,_) -> whd_ise1_metas sigma c | c -> c diff --git a/kernel/typing.ml b/kernel/safe_typing.ml index db3d00302e..e523be5108 100644 --- a/kernel/typing.ml +++ b/kernel/safe_typing.ml @@ -233,6 +233,7 @@ let empty_environment = empty_env let universes = universes let context = context +let var_context = var_context let lookup_var = lookup_var let lookup_rel = lookup_rel @@ -283,7 +284,7 @@ let add_constant sp ce env = const_kind = kind_of_path sp; const_body = Some ce.const_entry_body; const_type = ty; - const_hyps = get_globals (context env); + const_hyps = var_context env; const_constraints = Constraint.union cst cst'; const_opaque = false } in @@ -296,7 +297,7 @@ let add_parameter sp t env = const_kind = kind_of_path sp; const_body = None; const_type = assumption_of_judgment env' Evd.empty jt; - const_hyps = get_globals (context env); + const_hyps = var_context env; const_constraints = cst; const_opaque = false } in diff --git a/kernel/typing.mli b/kernel/safe_typing.mli index 10530d123b..392040814f 100644 --- a/kernel/typing.mli +++ b/kernel/safe_typing.mli @@ -24,6 +24,7 @@ val empty_environment : environment val universes : environment -> universes val context : environment -> context +val var_context : environment -> var_context val push_var : identifier * constr -> environment -> environment val push_rel : name * constr -> environment -> environment diff --git a/kernel/sign.ml b/kernel/sign.ml index 5d7d5309b0..0b34c7edf3 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -10,7 +10,7 @@ open Term type 'a signature = identifier list * 'a list type 'a db_signature = (name * 'a) list -type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature +type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature let gLOB hyps = ENVIRON (hyps,[]) @@ -233,7 +233,7 @@ let lookup_id id env = | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y) -type 'b assumptions = (typed_type,'b) env -type context = (typed_type,typed_type) env +type 'b assumptions = (typed_type,'b) sign +type context = (typed_type,typed_type) sign type var_context = typed_type signature diff --git a/kernel/sign.mli b/kernel/sign.mli index 2a0a567dec..e2ef7d4a1e 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -54,35 +54,35 @@ val dbindv : 'a signature -> 'b term array -> 'a * 'b term (*s Signatures with named and de Bruijn variables. *) type 'a db_signature = (name * 'a) list -type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature - -val gLOB : 'b signature -> ('b,'a) env - -val add_rel : (name * 'a) -> ('b,'a) env -> ('b,'a) env -val add_glob : (identifier * 'b) -> ('b,'a) env -> ('b,'a) env -val lookup_glob : identifier -> ('b,'a) env -> (identifier * 'b) -val lookup_rel : int -> ('b,'a) env -> (name * 'a) -val mem_glob : identifier -> ('b,'a) env -> bool - -val get_globals : ('b,'a) env -> 'b signature -val get_rels : ('b,'a) env -> 'a db_signature -val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) env -> 'c -> 'c -val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) env -> 'c -val map_rel_env : ('a -> 'b) -> ('c,'a) env -> ('c,'b) env -val map_var_env : ('c -> 'b) -> ('c,'a) env -> ('b,'a) env -val isnull_rel_env : ('a,'b) env -> bool -val uncons_rel_env : ('a,'b) env -> (name * 'b) * ('a,'b) env -val ids_of_env : ('a, 'b) env -> identifier list +type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature + +val gLOB : 'b signature -> ('b,'a) sign + +val add_rel : (name * 'a) -> ('b,'a) sign -> ('b,'a) sign +val add_glob : (identifier * 'b) -> ('b,'a) sign -> ('b,'a) sign +val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b) +val lookup_rel : int -> ('b,'a) sign -> (name * 'a) +val mem_glob : identifier -> ('b,'a) sign -> bool + +val get_globals : ('b,'a) sign -> 'b signature +val get_rels : ('b,'a) sign -> 'a db_signature +val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c +val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) sign -> 'c +val map_rel_env : ('a -> 'b) -> ('c,'a) sign -> ('c,'b) sign +val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign +val isnull_rel_env : ('a,'b) sign -> bool +val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign +val ids_of_env : ('a, 'b) sign -> identifier list type ('b,'a) search_result = | GLOBNAME of identifier * 'b | RELNAME of int * 'a -val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result +val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result -type 'b assumptions = (typed_type,'b) env -type context = (typed_type,typed_type) env +type 'b assumptions = (typed_type,'b) sign +type context = (typed_type,typed_type) sign type var_context = typed_type signature val unitize_env : 'a assumptions -> unit assumptions diff --git a/kernel/typeops.ml b/kernel/typeops.ml index d224b0209e..0d2d5cba50 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -75,14 +75,14 @@ let hyps_inclusion env sigma (idl1,tyl1) (idl2,tyl2) = current context of [env]. *) let construct_reference id env sigma hyps = - let hyps' = get_globals (context env) in + let hyps' = var_context env in if hyps_inclusion env sigma hyps hyps' then Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)) else error_reference_variables CCI env id let check_hyps id env sigma hyps = - let hyps' = get_globals (context env) in + let hyps' = var_context env in if not (hyps_inclusion env sigma hyps hyps') then error_reference_variables CCI env id @@ -178,7 +178,7 @@ let type_inst_construct env sigma i mind = let type_of_existential env sigma c = let (ev,args) = destEvar c in let evi = Evd.map sigma ev in - let hyps = get_globals (context evi.Evd.evar_env) in + let hyps = var_context evi.Evd.evar_env in let id = id_of_string ("?" ^ string_of_int ev) in check_hyps id env sigma hyps; instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args) |