aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml12
-rw-r--r--pretyping/classops.ml11
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/evarconv.ml10
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/evarsolve.ml12
-rw-r--r--pretyping/indrec.ml3
-rw-r--r--pretyping/nativenorm.ml12
-rw-r--r--pretyping/pretyping.ml33
-rw-r--r--pretyping/recordops.ml14
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/unification.ml4
12 files changed, 55 insertions, 66 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9fa8442f8a..54e847988b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -994,8 +994,8 @@ let expand_arg tms (p,ccl) ((_,t),_,na) =
let k = length_of_tomatch_type_sign na t in
(p+k,liftn_predicate (k-1) (p+1) ccl tms)
-let use_unit_judge evd =
- let j, ctx = coq_unit_judge () in
+let use_unit_judge env evd =
+ let j, ctx = coq_unit_judge !!env in
let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in
evd', j
@@ -1024,7 +1024,7 @@ let adjust_impossible_cases sigma pb pred tomatch submat =
| Evar (evk,_) when snd (evar_source evk sigma) == Evar_kinds.ImpossibleCase ->
let sigma =
if not (Evd.is_defined sigma evk) then
- let sigma, default = use_unit_judge sigma in
+ let sigma, default = use_unit_judge pb.env sigma in
let sigma = Evd.define evk default.uj_type sigma in
sigma
else sigma
@@ -2512,7 +2512,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
(predopt, tomatchl, eqns) =
let typing_fun tycon env sigma = function
| Some t -> typing_function tycon env sigma t
- | None -> use_unit_judge sigma in
+ | None -> use_unit_judge env sigma in
(* We build the matrix of patterns and right-hand side *)
let matx = matx_of_eqns env eqns in
@@ -2593,7 +2593,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
let typing_function tycon env sigma = function
| Some t -> typing_function tycon env sigma t
- | None -> use_unit_judge sigma in
+ | None -> use_unit_judge env sigma in
let pb =
{ env = env;
@@ -2668,7 +2668,7 @@ let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, e
(* A typing function that provides with a canonical term for absurd cases*)
let typing_fun tycon env sigma = function
| Some t -> typing_fun tycon env sigma t
- | None -> use_unit_judge sigma in
+ | None -> use_unit_judge env sigma in
let pb =
{ env = env;
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b026397abf..73141191cf 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -15,7 +15,6 @@ open Names
open Constr
open Libnames
open Globnames
-open Nametab
open Libobject
open Mod_subst
@@ -228,14 +227,14 @@ let string_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
| CL_CONST sp ->
- string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+ string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp))
| CL_PROJ sp ->
let sp = Projection.Repr.constant sp in
- string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+ string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp))
| CL_IND sp ->
- string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp))
+ string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp))
| CL_SECVAR sp ->
- string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp))
+ string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp))
let pr_class x = str (string_of_class x)
@@ -520,7 +519,7 @@ module CoercionPrinting =
let compare = GlobRef.Ordered.compare
let encode = coercion_of_reference
let subst = subst_coe_typ
- let printer x = pr_global_env Id.Set.empty x
+ let printer x = Nametab.pr_global_env Id.Set.empty x
let key = ["Printing";"Coercion"]
let title = "Explicitly printed coercions: "
let member_message x b =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0dc5a9bad5..072ac9deed 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -25,7 +25,6 @@ open Termops
open Namegen
open Libnames
open Globnames
-open Nametab
open Mod_subst
open Decl_kinds
open Context.Named.Declaration
@@ -58,7 +57,7 @@ let add_name_opt na b t (nenv, env) =
(* Tools for printing of Cases *)
let encode_inductive r =
- let indsp = global_inductive r in
+ let indsp = Nametab.global_inductive r in
let constr_lengths = constructors_nrealargs indsp in
(indsp,constr_lengths)
@@ -97,7 +96,7 @@ module PrintingInductiveMake =
let compare = ind_ord
let encode = Test.encode
let subst subst obj = subst_ind subst obj
- let printer ind = pr_global_env Id.Set.empty (IndRef ind)
+ let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind)
let key = ["Printing";Test.field]
let title = Test.title
let member_message x = Test.member_message (printer x)
@@ -647,6 +646,7 @@ and detype_r d flags avoid env sigma t =
else
GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
| Var id ->
+ (* Discriminate between section variable and non-section variable *)
(try let _ = Global.lookup_named id in GRef (VarRef id, None)
with Not_found -> GVar id)
| Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s))
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 72d95f7eb1..f0ff1aa93b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -46,14 +46,14 @@ let _ = Goptions.declare_bool_option {
(*******************************************)
(* Functions to deal with impossible cases *)
(*******************************************)
-let impossible_default_case () =
+let impossible_default_case env =
let type_of_id =
let open Names.GlobRef in
match Coqlib.lib_ref "core.IDProp.type" with
| ConstRef c -> c
| VarRef _ | IndRef _ | ConstructRef _ -> assert false
in
- let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Coqlib.(lib_ref "core.IDProp.idProp")) in
+ let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in
let (_, u) = Constr.destConst c in
Some (c, Constr.mkConstU (type_of_id, u), ctx)
@@ -62,8 +62,8 @@ let coq_unit_judge =
let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
let na1 = Name (Id.of_string "A") in
let na2 = Name (Id.of_string "H") in
- fun () ->
- match impossible_default_case () with
+ fun env ->
+ match impossible_default_case env with
| Some (id, type_of_id, ctx) ->
make_judge id type_of_id, ctx
| None ->
@@ -1352,7 +1352,7 @@ let solve_unconstrained_impossible_cases env evd =
Evd.fold_undefined (fun evk ev_info evd' ->
match ev_info.evar_source with
| loc,Evar_kinds.ImpossibleCase ->
- let j, ctx = coq_unit_judge () in
+ let j, ctx = coq_unit_judge env in
let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
let ty = j_type j in
let conv_algo = evar_conv_x full_transparent_state in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 20a4f34ec7..350dece28a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -80,4 +80,4 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool ->
(**/**)
(** {6 Functions to deal with impossible cases } *)
-val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
+val coq_unit_judge : env -> EConstr.unsafe_judgment Univ.in_universe_context_set
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6f5cba3e03..22f438c00c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -425,7 +425,7 @@ let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t w
let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma)
-let free_vars_and_rels_up_alias_expansion sigma aliases c =
+let free_vars_and_rels_up_alias_expansion env sigma aliases c =
let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
@@ -457,7 +457,7 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
| Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
| _ -> frec (aliases,depth) c end
| Const _ | Ind _ | Construct _ ->
- acc2 := Id.Set.union (vars_of_global (Global.env()) (EConstr.to_constr sigma c)) !acc2
+ acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2
| _ ->
iter_with_full_binders sigma
(fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
@@ -488,13 +488,13 @@ let alias_distinct l =
in
check (Int.Set.empty, Id.Set.empty) l
-let get_actual_deps evd aliases l t =
+let get_actual_deps env evd aliases l t =
if occur_meta_or_existential evd t then
(* Probably no restrictions on allowed vars in presence of evars *)
l
else
(* Probably strong restrictions coming from t being evar-closed *)
- let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion evd aliases t in
+ let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion env evd aliases t in
List.filter (function
| VarAlias id -> Id.Set.mem id fv_ids
| RelAlias n -> Int.Set.mem n fv_rels
@@ -520,7 +520,7 @@ let remove_instance_local_defs evd evk args =
let find_unification_pattern_args env evd l t =
let aliases = make_alias_map env evd in
match expand_and_check_vars evd aliases l with
- | Some l as x when alias_distinct (get_actual_deps evd aliases l t) -> x
+ | Some l as x when alias_distinct (get_actual_deps env evd aliases l t) -> x
| _ -> None
let is_unification_pattern_meta env evd nb m l t =
@@ -1202,7 +1202,7 @@ exception EvarSolvedOnTheFly of evar_map * EConstr.constr
the common domain of definition *)
let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
(* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
- let fvs2 = free_vars_and_rels_up_alias_expansion evd aliases (mkEvar ev2) in
+ let fvs2 = free_vars_and_rels_up_alias_expansion env evd aliases (mkEvar ev2) in
let filter1 = restrict_upon_filter evd evk1
(has_constrainable_free_vars env evd aliases force k2 evk2 fvs2)
argsv1 in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e49ba75b3f..89f64d328a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -29,7 +29,6 @@ open Inductive
open Inductiveops
open Environ
open Reductionops
-open Nametab
open Context.Rel.Declaration
type dep_flag = bool
@@ -618,6 +617,6 @@ let lookup_eliminator ind_sp s =
user_err ~hdr:"default_elim"
(strbrk "Cannot find the elimination combinator " ++
Id.print id ++ strbrk ", the elimination of the inductive definition " ++
- pr_global_env Id.Set.empty (IndRef ind_sp) ++
+ Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++
strbrk " on sort " ++ Termops.pr_sort_family s ++
strbrk " is probably not allowed.")
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 20185363e6..022c383f60 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -132,15 +132,15 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
(mkApp(mkConstructU((ind,i),u), params), ctyp)
-let construct_of_constr const env tag typ =
+let construct_of_constr const env sigma tag typ =
let t, l = app_type env typ in
- match kind t with
+ match EConstr.kind_upto sigma t with
| Ind (ind,u) ->
construct_of_constr_notnative const env tag ind u l
| _ -> assert false
-let construct_of_constr_const env tag typ =
- fst (construct_of_constr true env tag typ)
+let construct_of_constr_const env sigma tag typ =
+ fst (construct_of_constr true env sigma tag typ)
let construct_of_constr_block = construct_of_constr false
@@ -207,9 +207,9 @@ let rec nf_val env sigma v typ =
let env = push_rel (LocalAssum (name,dom)) env in
let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
mkLambda(name,dom,body)
- | Vconst n -> construct_of_constr_const env n typ
+ | Vconst n -> construct_of_constr_const env sigma n typ
| Vblock b ->
- let capp,ctyp = construct_of_constr_block env (block_tag b) typ in
+ let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in
let args = nf_bargs env sigma b ctyp in
mkApp(capp,args)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 495f5c0660..f2881e4a19 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -405,32 +405,25 @@ let interp_glob_level ?loc evd : glob_level -> _ = function
| GSet -> evd, Univ.Level.set
| GType s -> interp_level_info ?loc evd s
-let interp_instance ?loc evd ~len l =
- if len != List.length l then
+let interp_instance ?loc evd l =
+ let evd, l' =
+ List.fold_left
+ (fun (evd, univs) l ->
+ let evd, l = interp_glob_level ?loc evd l in
+ (evd, l :: univs)) (evd, [])
+ l
+ in
+ if List.exists (fun l -> Univ.Level.is_prop l) l' then
user_err ?loc ~hdr:"pretype"
- (str "Universe instance should have length " ++ int len)
- else
- let evd, l' =
- List.fold_left
- (fun (evd, univs) l ->
- let evd, l = interp_glob_level ?loc evd l in
- (evd, l :: univs)) (evd, [])
- l
- in
- if List.exists (fun l -> Univ.Level.is_prop l) l' then
- user_err ?loc ~hdr:"pretype"
- (str "Universe instances cannot contain Prop, polymorphic" ++
- str " universe instances must be greater or equal to Set.");
- evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+ (str "Universe instances cannot contain Prop, polymorphic" ++
+ str " universe instances must be greater or equal to Set.");
+ evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
let pretype_global ?loc rigid env evd gr us =
let evd, instance =
match us with
| None -> evd, None
- | Some l ->
- let _, ctx = Global.constr_of_global_in_context !!env gr in
- let len = Univ.AUContext.size ctx in
- interp_instance ?loc evd ~len l
+ | Some l -> interp_instance ?loc evd l
in
Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3719f9302a..5d74b59b27 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -20,7 +20,6 @@ open Util
open Pp
open Names
open Globnames
-open Nametab
open Constr
open Libobject
open Mod_subst
@@ -230,8 +229,7 @@ let warn_projection_no_head_constant =
++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
(* Intended to always succeed *)
-let compute_canonical_projections warn (con,ind) =
- let env = Global.env () in
+let compute_canonical_projections env warn (con,ind) =
let ctx = Environ.constant_context env con in
let u = Univ.make_abstract_instance ctx in
let v = (mkConstU (con,u)) in
@@ -282,7 +280,10 @@ let warn_redundant_canonical_projection =
++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
let add_canonical_structure warn o =
- let lo = compute_canonical_projections warn o in
+ (* XXX: Undesired global access to env *)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let lo = compute_canonical_projections env warn o in
List.iter (fun ((proj,(cs_pat,_ as pat)),s) ->
let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
let ocs = try Some (assoc_pat cs_pat l)
@@ -290,9 +291,6 @@ let add_canonical_structure warn o =
in match ocs with
| None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table;
| Some (c, cs) ->
- (* XXX: Undesired global access to env *)
- let env = Global.env () in
- let sigma = Evd.from_env env in
let old_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF))
and new_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF))
in
@@ -331,7 +329,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
let error_not_structure ref description =
user_err ~hdr:"object_declare"
(str"Could not declare a canonical structure " ++
- (Id.print (basename_of_global ref) ++ str"." ++ spc() ++
+ (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++
description))
let check_and_decompose_canonical_structure ref =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 7e5815acd1..ce12aaeeb0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -320,7 +320,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
hints @ (path', info, body) :: rest
in List.fold_left declare_proj [] projs
in
- let term = UnivGen.constr_of_global_univ (glob, inst) in
+ let term = Constr.mkRef (glob, inst) in
(*FIXME subclasses should now get substituted for each particular instance of
the polymorphic superclass *)
aux pri term ty [glob]
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4665486fc0..e3b942b610 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1417,7 +1417,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
and mimick_undefined_evar evd flags hdc nargs sp =
let ev = Evd.find_undefined evd sp in
- let sp_env = Global.env_of_context (evar_filtered_hyps ev) in
+ let sp_env = reset_with_named_context (evar_filtered_hyps ev) env in
let (evd', c) = applyHead sp_env evd nargs hdc in
let (evd'',mc,ec) =
unify_0 sp_env evd' CUMUL flags
@@ -1633,7 +1633,7 @@ let make_eq_test env evd c =
let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let id =
let t = match ty with Some t -> t | None -> get_type_of env sigma c in
- let x = id_of_name_using_hdchar (Global.env()) sigma t name in
+ let x = id_of_name_using_hdchar env sigma t name in
let ids = Environ.ids_of_named_context_val (named_context_val env) in
if name == Anonymous then next_ident_away_in_goal x ids else
if mem_named_context_val x (named_context_val env) then
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 22:25:36 +0000