aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-05-28 13:38:23 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-05-28 13:38:23 +0200
commit81535edc4b21015bd63d23e57ca9d707b4b71f6b (patch)
tree6a76bc46b66cade1b53d2c878ae2aa7c5e1f5dc5
parentb2f746e41abf53fc481f90804ba4d70edd73fc86 (diff)
parentdfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (diff)
Merge PR #7419: Remove 100 occurrences of Evd.empty
-rw-r--r--dev/base_include4
-rw-r--r--dev/top_printers.ml4
-rw-r--r--engine/termops.ml17
-rw-r--r--ide/idetop.ml7
-rw-r--r--interp/impargs.ml8
-rw-r--r--interp/notation_ops.ml4
-rw-r--r--interp/reserve.ml4
-rw-r--r--plugins/firstorder/sequent.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml10
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--plugins/ltac/extratactics.ml416
-rw-r--r--plugins/ltac/pptactic.ml7
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/omega/coq_omega.ml7
-rw-r--r--plugins/ssr/ssrvernac.ml45
-rw-r--r--plugins/ssrmatching/ssrmatching.ml46
-rw-r--r--pretyping/detyping.ml8
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/patternops.ml8
-rw-r--r--pretyping/pretype_errors.ml2
-rw-r--r--pretyping/recordops.ml8
-rw-r--r--printing/prettyp.ml9
-rw-r--r--printing/printer.ml4
-rw-r--r--printing/printmod.ml9
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/eqschemes.ml10
-rw-r--r--tactics/hints.ml8
-rw-r--r--tactics/inv.ml5
-rw-r--r--vernac/class.ml2
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comDefinition.ml4
-rw-r--r--vernac/comFixpoint.ml2
-rw-r--r--vernac/comInductive.ml8
-rw-r--r--vernac/himsg.ml35
-rw-r--r--vernac/obligations.ml20
-rw-r--r--vernac/record.ml4
-rw-r--r--vernac/search.ml14
-rw-r--r--vernac/vernacentries.ml4
41 files changed, 179 insertions, 114 deletions
diff --git a/dev/base_include b/dev/base_include
index 2f5d8aa84..8d81ca3e0 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -204,7 +204,9 @@ let e s =
implicit syntax *)
let constr_of_string s =
- Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);;
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Constrintern.interp_constr env sigma (parse_constr s);;
(* get the body of a constant *)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index cb1abc4a9..129f171b2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -221,7 +221,9 @@ let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c)
let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
let ppnamedcontextval e =
- pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pp (pr_named_context env sigma (named_context_of_val e))
let ppenv e = pp
(str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
diff --git a/engine/termops.ml b/engine/termops.ml
index 053fcc3db..bd07555a5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -98,7 +98,10 @@ let rec pr_constr c = match kind c with
let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
let print_constr_env env sigma t = !term_printer env sigma t
-let print_constr t = !term_printer (Global.env()) Evd.empty t
+let print_constr t =
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ !term_printer env evd t
let set_print_constr f = term_printer := f
module EvMap = Evar.Map
@@ -340,7 +343,7 @@ let pr_evar_constraints sigma pbs =
str (match pbty with
| Reduction.CONV -> "=="
| Reduction.CUMUL -> "<=") ++
- spc () ++ protect (print_constr_env env Evd.empty) t2
+ spc () ++ protect (print_constr_env env @@ Evd.from_env env) t2
in
prlist_with_sep fnl pr_evconstr pbs
@@ -434,27 +437,29 @@ let pr_metaset metas =
let pr_var_decl env decl =
let open NamedDecl in
+ let evd = Evd.from_env env in
let pbody = match decl with
| LocalAssum _ -> mt ()
| LocalDef (_,c,_) ->
(* Force evaluation *)
let c = EConstr.of_constr c in
- let pb = print_constr_env env Evd.empty c in
+ let pb = print_constr_env env evd c in
(str" := " ++ pb ++ cut () ) in
- let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
+ let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
let ptyp = (str" : " ++ pt) in
(Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp))
let pr_rel_decl env decl =
let open RelDecl in
+ let evd = Evd.from_env env in
let pbody = match decl with
| LocalAssum _ -> mt ()
| LocalDef (_,c,_) ->
(* Force evaluation *)
let c = EConstr.of_constr c in
- let pb = print_constr_env env Evd.empty c in
+ let pb = print_constr_env env evd c in
(str":=" ++ spc () ++ pb ++ spc ()) in
- let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
+ let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
match get_name decl with
| Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
| Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 64f165cde..ba69c4185 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -272,7 +272,10 @@ let status force =
let export_coq_object t = {
Interface.coq_object_prefix = t.Search.coq_object_prefix;
Interface.coq_object_qualid = t.Search.coq_object_qualid;
- Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
+ Interface.coq_object_object =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Pp.string_of_ppcmds (pr_lconstr_env env sigma t.Search.coq_object_object)
}
let pattern_of_string ?env s =
@@ -282,7 +285,7 @@ let pattern_of_string ?env s =
| Some e -> e
in
let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
- let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in
+ let (_, pat) = Constrintern.intern_constr_pattern env (Evd.from_env env) constr in
pat
let dirpath_of_string_list s =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 2db67c299..8aa1e6250 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -237,11 +237,11 @@ let is_rigid env sigma t =
is_rigid_head sigma t
| _ -> true
-let find_displayed_name_in all avoid na (env, b) =
+let find_displayed_name_in sigma all avoid na (env, b) =
let envnames_b = (env, b) in
let flag = RenamingElsewhereFor envnames_b in
- if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
- else compute_displayed_name_in Evd.empty flag avoid na b
+ if all then compute_and_force_displayed_name_in sigma flag avoid na b
+ else compute_displayed_name_in sigma flag avoid na b
let compute_implicits_names_gen all env sigma t =
let open Context.Rel.Declaration in
@@ -249,7 +249,7 @@ let compute_implicits_names_gen all env sigma t =
let t = whd_all env sigma t in
match kind sigma t with
| Prod (na,a,b) ->
- let na',avoid' = find_displayed_name_in all avoid na (names,b) in
+ let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in
aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
| _ -> List.rev names
in aux env Id.Set.empty [] t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index e51c69136..448881dcf 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -509,7 +509,9 @@ let notation_constr_of_glob_constr nenv a =
let notation_constr_of_constr avoiding t =
let t = EConstr.of_constr t in
- let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let t = Detyping.detype Detyping.Now false avoiding env evd t in
let nenv = {
ninterp_var_type = Id.Map.empty;
ninterp_rec_vars = Id.Map.empty;
diff --git a/interp/reserve.ml b/interp/reserve.ml
index b57103cf2..071248f01 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -112,7 +112,9 @@ let revert_reserved_type t =
let t = EConstr.Unsafe.to_constr t in
let reserved = KeyMap.find (constr_key t) !reserve_revtable in
let t = EConstr.of_constr t in
- let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let t = Detyping.detype Detyping.Now false Id.Set.empty env evd t in
(* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
then I've introduced a bug... *)
let filter _ pat =
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 0c752d4a4..2a527da9b 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -229,7 +229,9 @@ let extend_with_auto_hints env sigma l seq =
let print_cmap map=
let print_entry c l s=
- let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
str "| " ++
prlist Printer.pr_global l ++
str " : " ++
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5e0d3e8ee..83fe1fc2f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -230,7 +230,7 @@ let isAppConstruct ?(env=Global.env ()) sigma t =
with Not_found -> false
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
+ Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env
exception NoChange
@@ -1099,10 +1099,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let get_body const =
match Global.body_of_constant const with
| Some (body, _) ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- (Global.env ())
- (Evd.empty)
+ env
+ sigma
(EConstr.of_constr body)
| None -> user_err Pp.(str "Cannot define a principle over an axiom ")
in
@@ -1340,7 +1342,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota (pf_env g) Evd.empty
+ Reductionops.nf_betaiota (pf_env g) (project g)
(applist(fbody_with_full_params,
(List.rev_map var_of_decl princ_params)@
(List.rev_map mkVar args_id)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 90af20b4c..d193e1144 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -38,7 +38,9 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
match opt_c with
| None -> mt ()
| Some b ->
- let (_, b) = b (Global.env ()) Evd.empty in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let (_, b) = b env evd in
spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b9d5ebf57..cc92a73f0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -67,7 +67,7 @@ let observe_tac s tac g =
let nf_zeta =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
Environ.empty_env
- Evd.empty
+ (Evd.from_env Environ.empty_env)
let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ab03f1831..72bb8253d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -106,12 +106,12 @@ let const_of_ref = function
let nf_zeta env =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- env
- Evd.empty
+ env (Evd.from_env env)
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
+ Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env
+ (Evd.from_env Environ.empty_env)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 797dfbe23..c21921513 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -613,10 +613,12 @@ END
VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
| [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
- [ let tc,_ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in
- let tb,_ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in
- let tc = EConstr.to_constr Evd.empty tc in
- let tb = EConstr.to_constr Evd.empty tb in
+ [ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let tc,_ctx = Constrintern.interp_constr env evd c in
+ let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in
+ let tc = EConstr.to_constr evd tc in
+ let tb = EConstr.to_constr evd tb in
Global.register f tc tb ]
END
@@ -779,7 +781,7 @@ let mkCaseEq a : unit Proofview.tactic =
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
(** FIXME: this looks really wrong. Does anybody really use this tactic? *)
- let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl in
+ let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in
change_concl c
end;
simplest_case a]
@@ -1106,7 +1108,9 @@ END
VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [
let get_key c =
- let (evd, c) = Constrintern.interp_open_constr (Global.env ()) Evd.empty c in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let (evd, c) = Constrintern.interp_open_constr env evd c in
let kind c = EConstr.kind evd c in
Keys.constr_key kind c
in
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index bd02d85d5..3dfe308a5 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -149,9 +149,12 @@ let string_of_genarg_arg (ArgumentType arg) =
let open Genprint in
match generic_top_print (in_gen (Topwit wit) x) with
| TopPrinterBasic pr -> pr ()
- | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+ | TopPrinterNeedsContext pr ->
+ let env = Global.env() in
+ pr env (Evd.from_env env)
| TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
- printer (Global.env()) Evd.empty default_ensure_surrounded
+ let env = Global.env() in
+ printer env (Evd.from_env env) default_ensure_surrounded
end
| _ -> default
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1b86583da..b91315aca 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m =
let evd = solve_constraints env !evd in
let evd = Evd.minimize_universes evd in
let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
- Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m);
+ Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m);
Evd.evar_universe_context evd, m
let default_morphism sign m =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e455ebb28..3594c8765 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -369,8 +369,11 @@ let coq_True = lazy (init_constant "True")
(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
(* For unfold *)
-let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with
- | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
+let evaluable_ref_of_constr s c =
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ match EConstr.kind evd (Lazy.force c) with
+ | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) ->
EvalConstRef kn
| _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant."))
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 05dbf0a86..7ac9ea89d 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -377,7 +377,10 @@ let interp_head_pat hpat =
| Cast (c', _, _) -> loop c'
| Prod (_, _, c') -> loop c'
| LetIn (_, _, _, c') -> loop c'
- | _ -> Constr_matching.is_matching (Global.env()) Evd.empty p (EConstr.of_constr c) in
+ | _ ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Constr_matching.is_matching env sigma p (EConstr.of_constr c) in
filter_head, loop
let all_true _ = true
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 0dd3625ba..93c63d522 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -708,9 +708,9 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
;;
-let fixed_upat = function
+let fixed_upat evd = function
| {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false
-| {up_t = t} -> not (occur_existential Evd.empty (EConstr.of_constr t)) (** FIXME *)
+| {up_t = t} -> not (occur_existential evd (EConstr.of_constr t)) (** FIXME *)
let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())
@@ -769,7 +769,7 @@ let mk_tpattern_matcher ?(all_instances=false)
let p2t p = mkApp(p.up_f,p.up_a) in
let source () = match upats_origin, upats with
| None, [p] ->
- (if fixed_upat p then str"term " else str"partial term ") ++
+ (if fixed_upat ise p then str"term " else str"partial term ") ++
pr_constr_pat (p2t p) ++ spc()
| Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++
pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl()
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 779508477..fc398df9a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -929,9 +929,11 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
let rec subst_glob_constr subst = DAst.map (function
| GRef (ref,u) as raw ->
- let ref',t = subst_global subst ref in
- if ref' == ref then raw else
- DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t))
+ let ref',t = subst_global subst ref in
+ if ref' == ref then raw else
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t))
| GSort _
| GVar _
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 40f4d4ff8..27b029aad 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -42,7 +42,7 @@ type recursion_scheme_error =
exception RecursionSchemeError of recursion_scheme_error
-let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na
+let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na
let name_assumption env = function
| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 375ed10d0..9342b4cc7 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -279,9 +279,11 @@ let lift_pattern k = liftn_pattern k 1
let rec subst_pattern subst pat =
match pat with
| PRef ref ->
- let ref',t = subst_global subst ref in
- if ref' == ref then pat else
- pattern_of_constr (Global.env()) Evd.empty t
+ let ref',t = subst_global subst ref in
+ if ref' == ref then pat else
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ pattern_of_constr env evd t
| PVar _
| PEvar _
| PRel _ -> pat
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 278a4761d..856894d9a 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -165,7 +165,7 @@ let error_not_product ?loc env sigma c =
(*s Error in conversion from AST to glob_constr *)
let error_var_not_found ?loc s =
- raise_pretype_error ?loc (empty_env, Evd.empty, VarNotFound s)
+ raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s)
(*s Typeclass errors *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 9eb410f06..56a883099 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -199,7 +199,7 @@ let warn_projection_no_head_constant =
let env = Termops.push_rels_assum sign env in
let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
- let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in
+ let term_pp = Termops.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
strbrk "Projection value has no head constant: "
++ term_pp ++ strbrk " in canonical instance "
++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
@@ -211,7 +211,7 @@ let compute_canonical_projections warn (con,ind) =
let u = Univ.make_abstract_instance ctx in
let v = (mkConstU (con,u)) in
let c = Environ.constant_value_in env (con,u) in
- let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
+ let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in
let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
let t = EConstr.Unsafe.to_constr t in
let lt = List.rev_map snd sign in
@@ -317,7 +317,9 @@ let check_and_decompose_canonical_structure ref =
let vc = match Environ.constant_opt_value_in env (sp, u) with
| Some vc -> vc
| None -> error_not_structure ref "Could not find its value in the global environment." in
- let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in
let body = EConstr.Unsafe.to_constr body in
let f,args = match kind body with
| App (f,args) -> f,args
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index d036fec21..895181bc5 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -77,7 +77,9 @@ let print_ref reduce ref udecl =
let typ = EConstr.of_constr typ in
let typ =
if reduce then
- let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
in EConstr.it_mkProd_or_LetIn ccl ctx
else typ in
let univs = Global.universes_of_global ref in
@@ -717,7 +719,10 @@ let print_eval x = !object_pr.print_eval x
(**** Printing declarations and judgments *)
(**** Abstract layer *****)
-let print_typed_value x = print_typed_value_in_env (Global.env ()) Evd.empty x
+let print_typed_value x =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ print_typed_value_in_env env sigma x
let print_judgment env sigma {uj_val=trm;uj_type=typ} =
print_typed_value_in_env env sigma (trm, typ)
diff --git a/printing/printer.ml b/printing/printer.ml
index 88a1ab729..72030dc9f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -299,8 +299,8 @@ let pr_puniverses f env (c,u) =
let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
let pr_existential_key = Termops.pr_existential_key
let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev)
-let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind)
-let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr)
+let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (mkConstruct cstr)
let pr_pconstant = pr_puniverses pr_constant
let pr_pinductive = pr_puniverses pr_inductive
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 3c805b327..be8bc1357 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -323,7 +323,6 @@ let print_body is_impl env mp (l,body) =
else Univ.Instance.empty
in
let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
- let sigma = Evd.empty in
(match cb.const_body with
| Def _ -> def "Definition" ++ spc ()
| OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
@@ -332,17 +331,17 @@ let print_body is_impl env mp (l,body) =
| None -> mt ()
| Some env ->
str " :" ++ spc () ++
- hov 0 (Printer.pr_ltype_env env sigma
+ hov 0 (Printer.pr_ltype_env env (Evd.from_env env)
(Vars.subst_instance_constr u
cb.const_type)) ++
(match cb.const_body with
| Def l when is_impl ->
spc () ++
hov 2 (str ":= " ++
- Printer.pr_lconstr_env env sigma
+ Printer.pr_lconstr_env env (Evd.from_env env)
(Vars.subst_instance_constr u (Mod_subst.force_constr l)))
| _ -> mt ()) ++ str "." ++
- Printer.pr_universe_ctx sigma ctx)
+ Printer.pr_universe_ctx (Evd.from_env env) ctx)
| SFBmind mib ->
try
let env = Option.get env in
@@ -387,7 +386,7 @@ let rec print_typ_expr env mp locals mty =
let s = String.concat "." (List.map Id.to_string idl) in
(* XXX: What should env and sigma be here? *)
let env = Global.env () in
- let sigma = Evd.empty in
+ let sigma = Evd.from_env env in
hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
++ Printer.pr_lconstr_env env sigma c)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ea5d4719c..3e08c6d87 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1174,7 +1174,7 @@ let solve_inst env evd filter unique split fail =
let _ =
Hook.set Typeclasses.solve_all_instances_hook solve_inst
-let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
+let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
let (gl,t,sigma) =
Goal.V82.mk_goal sigma nc gl Store.empty in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 715686ad0..eede13329 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -78,7 +78,7 @@ let build_dependent_inductive ind (mib,mip) =
Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt
@ Context.Rel.to_extended_list mkRel 0 realargs)
-let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na
+let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na
let name_assumption env = function
| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
@@ -109,7 +109,7 @@ let get_coq_eq ctx =
let univ_of_eq env eq =
let eq = EConstr.of_constr eq in
- match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
+ match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) eq)) with
| Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false)
| _ -> assert false
@@ -620,7 +620,9 @@ let build_r2l_forward_rew_scheme dep env ind kind =
(**********************************************************************)
let fix_r2l_forward_rew_scheme (c, ctx') =
- let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
let t = EConstr.Unsafe.to_constr t in
let ctx,_ = decompose_prod_assum t in
match ctx with
@@ -630,7 +632,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
(mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
(mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
(mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
- (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty
+ (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma
(EConstr.of_constr (applist (c,
Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
in c', ctx'
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3ade5314b..786760122 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1263,7 +1263,9 @@ let prepare_hint check (poly,local) env init (sigma,c) =
subst := (evar,mkVar id)::!subst;
mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in
let c' = iter c in
- if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
+ let env = Global.env () in
+ let empty_sigma = Evd.from_env env in
+ if check then Pretyping.check_evars env empty_sigma sigma c';
let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
if poly then IsConstr (c', diff)
else if local then IsConstr (c', diff)
@@ -1276,7 +1278,9 @@ let interp_hints poly =
let sigma = Evd.from_env env in
let f poly c =
let evd,c = Constrintern.interp_open_constr env sigma c in
- prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ prepare_hint true (poly,false) env sigma (evd,c) in
let fref r =
let gr = global_with_alias r in
Dumpglob.add_glob ?loc:r.CAst.loc gr;
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 412954989..b346ed223 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -292,7 +292,7 @@ let error_too_many_names pats =
str "Unexpected " ++
str (String.plural (List.length pats) "introduction pattern") ++
str ": " ++ pr_enum (Miscprint.pr_intro_pattern
- (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
+ (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env (Evd.from_env env)))))) pats ++
str ".")
let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with
@@ -496,9 +496,10 @@ let wrap_inv_error id = function (e, info) -> match e with
| Indrec.RecursionSchemeError
(Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) ->
Proofview.tclENV >>= fun env ->
+ Proofview.tclEVARMAP >>= fun sigma ->
tclZEROMSG (
(strbrk "Inversion would require case analysis on sort " ++
- pr_sort Evd.empty k ++
+ pr_sort sigma k ++
strbrk " which is not allowed for inductive definition " ++
pr_inductive env (fst i) ++ str "."))
| e -> Proofview.tclZERO ~info e
diff --git a/vernac/class.ml b/vernac/class.ml
index 06e1694f9..133726702 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -67,7 +67,7 @@ let explain_coercion_error g = function
let check_reference_arity ref =
let env = Global.env () in
let c, _ = Global.type_of_global_in_context env ref in
- if not (Reductionops.is_arity env Evd.empty (EConstr.of_constr c)) (** FIXME *) then
+ if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (** FIXME *) then
raise (CoercionError (NotAClass ref))
let check_arity = function
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 61ce5d6c4..d99d45313 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -196,7 +196,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
let (_, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
let sigma = Evd.minimize_universes sigma in
- Pretyping.check_evars env Evd.empty sigma termtype;
+ Pretyping.check_evars env (Evd.from_env env) sigma termtype;
let univs = Evd.check_univ_decl ~poly sigma decl in
let termtype = to_constr sigma termtype in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
@@ -290,7 +290,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
(* Beware of this step, it is required as to minimize universes. *)
let sigma = Evd.minimize_universes sigma in
(* Check that the type is free of evars now. *)
- Pretyping.check_evars env Evd.empty sigma termtype;
+ Pretyping.check_evars env (Evd.from_env env) sigma termtype;
let termtype = to_constr sigma termtype in
let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
@@ -365,7 +365,7 @@ let context poly l =
let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in
(* Note, we must use the normalized evar from now on! *)
let sigma = Evd.minimize_universes sigma in
- let ce t = Pretyping.check_evars env Evd.empty sigma t in
+ let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
let ctx =
try named_of_rel_context fullctx
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 722f21171..492ae1d9b 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -157,7 +157,7 @@ let do_assumptions kind nl l =
((sigma,env,ienv),((is_coe,idl),t,imps)))
(sigma,env,empty_internalization_env) l
in
- let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in
+ let sigma = solve_remaining_evars all_and_fail_flags env sigma (Evd.from_env env) in
(* The universe constraints come from the whole telescope. *)
let sigma = Evd.minimize_universes sigma in
let nf_evar c = EConstr.to_constr sigma c in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 863adb0d1..2d4bd6779 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -104,7 +104,9 @@ let interp_definition pl bl poly red_option c ctypopt =
(red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
let check_definition (ce, evd, _, imps) =
- check_evars_are_solved (Global.env ()) evd Evd.empty;
+ let env = Global.env () in
+ let empty_sigma = Evd.from_env env in
+ check_evars_are_solved env evd empty_sigma;
ce
let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 85c0699ea..d996443d6 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -232,7 +232,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
(env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
let check_recursive isfix env evd (fixnames,fixdefs,_) =
- check_evars_are_solved env evd Evd.empty;
+ check_evars_are_solved env evd (Evd.from_env env);
if List.for_all Option.has_some fixdefs then begin
let fixdefs = List.map Option.get fixdefs in
check_mutuality env evd isfix (List.combine fixnames fixdefs)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 629fcce5a..790e83dbe 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,7 +367,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
() in
(* Try further to solve evars, and instantiate them *)
- let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in
+ let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in
(* Compute renewed arities *)
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
@@ -381,10 +381,10 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
let uctx = Evd.check_univ_decl ~poly sigma decl in
- List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities;
- Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params;
+ List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
+ Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
List.iter (fun (_,ctyps,_) ->
- List.iter (fun c -> check_evars env_ar_params Evd.empty sigma (EConstr.of_constr c)) ctyps)
+ List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
constructors;
(* Build the inductive entries *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 1add1f486..d4c5def6f 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -848,9 +848,9 @@ let explain_not_match_error = function
str "the body of definitions differs"
| NotConvertibleTypeField (env, typ1, typ2) ->
str "expected type" ++ spc () ++
- quote (Printer.safe_pr_lconstr_env env Evd.empty typ2) ++ spc () ++
+ quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) typ2) ++ spc () ++
str "but found type" ++ spc () ++
- quote (Printer.safe_pr_lconstr_env env Evd.empty typ1)
+ quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) typ1)
| NotSameConstructorNamesField ->
str "constructor names differ"
| NotSameInductiveNameInBlockField ->
@@ -889,9 +889,9 @@ let explain_not_match_error = function
Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
| IncompatiblePolymorphism (env, t1, t2) ->
str "conversion of polymorphic values generates additional constraints: " ++
- quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++
+ quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++
str "compared to " ++ spc () ++
- quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
+ quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2)
| IncompatibleConstraints cst ->
str " the expected (polymorphic) constraints do not imply " ++
let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in
@@ -1011,8 +1011,9 @@ let explain_module_internalization_error = function
(* Typeclass errors *)
let explain_not_a_class env c =
- let c = EConstr.to_constr Evd.empty c in
- pr_constr_env env Evd.empty c ++ str" is not a declared type class."
+ let sigma = Evd.from_env env in
+ let c = EConstr.to_constr sigma c in
+ pr_constr_env env sigma c ++ str" is not a declared type class."
let explain_unbound_method env cid { CAst.v = id } =
str "Unbound method name " ++ Id.print (id) ++ spc () ++
@@ -1025,7 +1026,7 @@ let pr_constr_exprs exprs =
let explain_mismatched_contexts env c i j =
str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
- hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env Evd.empty j) ++
+ hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env (Evd.from_env env) j) ++
fnl () ++ brk (1,1) ++
hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
@@ -1087,19 +1088,19 @@ let explain_refiner_error env sigma = function
(* Inductive errors *)
let error_non_strictly_positive env c v =
- let pc = pr_lconstr_env env Evd.empty c in
- let pv = pr_lconstr_env env Evd.empty v in
+ let pc = pr_lconstr_env env (Evd.from_env env) c in
+ let pv = pr_lconstr_env env (Evd.from_env env) v in
str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
brk(1,1) ++ pc ++ str "."
let error_ill_formed_inductive env c v =
- let pc = pr_lconstr_env env Evd.empty c in
- let pv = pr_lconstr_env env Evd.empty v in
+ let pc = pr_lconstr_env env (Evd.from_env env) c in
+ let pv = pr_lconstr_env env (Evd.from_env env) v in
str "Not enough arguments applied to the " ++ pv ++
str " in" ++ brk(1,1) ++ pc ++ str "."
let error_ill_formed_constructor env id c v nparams nargs =
- let pv = pr_lconstr_env env Evd.empty v in
+ let pv = pr_lconstr_env env (Evd.from_env env) v in
let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in
str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++
str "is not valid;" ++ brk(1,1) ++
@@ -1119,12 +1120,12 @@ let error_ill_formed_constructor env id c v nparams nargs =
let pr_ltype_using_barendregt_convention_env env c =
(* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
- quote (pr_goal_concl_style_env env Evd.empty (EConstr.of_constr c))
+ quote (pr_goal_concl_style_env env (Evd.from_env env) (EConstr.of_constr c))
let error_bad_ind_parameters env c n v1 v2 =
let pc = pr_ltype_using_barendregt_convention_env env c in
- let pv1 = pr_lconstr_env env Evd.empty v1 in
- let pv2 = pr_lconstr_env env Evd.empty v2 in
+ let pv1 = pr_lconstr_env env (Evd.from_env env) v1 in
+ let pv2 = pr_lconstr_env env (Evd.from_env env) v2 in
str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "."
@@ -1142,7 +1143,7 @@ let error_same_names_overlap idl =
prlist_with_sep pr_comma Id.print idl ++ str "."
let error_not_an_arity env c =
- str "The type" ++ spc () ++ pr_lconstr_env env Evd.empty c ++ spc () ++
+ str "The type" ++ spc () ++ pr_lconstr_env env (Evd.from_env env) c ++ spc () ++
str "is not an arity."
let error_bad_entry () =
@@ -1316,4 +1317,4 @@ let explain_reduction_tactic_error = function
str "The abstracted term" ++ spc () ++
quote (pr_goal_concl_style_env env sigma c) ++
spc () ++ str "is not well typed." ++ fnl () ++
- explain_type_error env' Evd.empty e
+ explain_type_error env' (Evd.from_env env') e
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 3bf0ca0a8..dfc51a990 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -266,7 +266,9 @@ let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
let error s = pperror (str s)
let reduce c =
- EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c))
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c))
exception NoObligations of Id.t option
@@ -521,8 +523,10 @@ let declare_mutual_definition l =
List.split3
(List.map (fun x ->
let subs, typ = (subst_body true x) in
- let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len (EConstr.of_constr subs)) in
- let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len (EConstr.of_constr typ)) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
+ let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
let term = EConstr.Unsafe.to_constr term in
let typ = EConstr.Unsafe.to_constr typ in
x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
@@ -1069,9 +1073,11 @@ let show_obligations_of_prg ?(msg=true) prg =
if !showed > 0 then (
decr showed;
let x = subst_deps_obl obls x in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
- hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
+ hov 1 (Printer.pr_constr_env env sigma x.obl_type ++
str "." ++ fnl ())))
| Some _ -> ())
obls
@@ -1087,9 +1093,11 @@ let show_obligations ?(msg=true) n =
let show_term n =
let prg = get_prog_err n in
let n = prg.prg_name in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
(Id.print n ++ spc () ++ str":" ++ spc () ++
- Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
- ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
+ Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+ ++ Printer.pr_constr_env env sigma prg.prg_body)
let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
diff --git a/vernac/record.ml b/vernac/record.ml
index bf6affd5f..5ff118473 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -152,7 +152,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
in
let sigma =
- Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma Evd.empty in
+ Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma (Evd.from_env env_ar) in
let sigma, typ =
let _, univ = compute_constructor_level sigma env_ar newfs in
if not def && (Sorts.is_prop sort ||
@@ -172,7 +172,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
let newfs = List.map (EConstr.to_rel_decl sigma) newfs in
let newps = List.map (EConstr.to_rel_decl sigma) newps in
let typ = EConstr.to_constr sigma typ in
- let ce t = Pretyping.check_evars env0 Evd.empty sigma (EConstr.of_constr t) in
+ let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in
let univs = Evd.check_univ_decl ~poly sigma decl in
let ubinders = Evd.universe_binders sigma in
List.iter (iter_constr ce) (List.rev newps);
diff --git a/vernac/search.ml b/vernac/search.ml
index 6d07187fe..e8ccec11c 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -215,7 +215,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref)
let search_about_filter query gr env typ = match query with
| GlobSearchSubPattern pat ->
- Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat (EConstr.of_constr typ)
+ Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ)
| GlobSearchString s ->
String.string_contains ~where:(name_of_reference gr) ~what:s
@@ -226,7 +226,7 @@ let search_pattern gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
- pattern_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) &&
+ pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
blacklist_filter ref env typ
in
let iter ref env typ =
@@ -250,8 +250,8 @@ let search_rewrite gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
- (pattern_filter pat1 ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) ||
- pattern_filter pat2 ref env Evd.empty (EConstr.of_constr typ)) &&
+ (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) ||
+ pattern_filter pat2 ref env (Evd.from_env env) (EConstr.of_constr typ)) &&
blacklist_filter ref env typ
in
let iter ref env typ =
@@ -265,7 +265,7 @@ let search_by_head gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
- head_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) &&
+ head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
blacklist_filter ref env typ
in
let iter ref env typ =
@@ -329,12 +329,12 @@ let interface_search =
toggle (Str.string_match regexp id 0) flag
in
let match_type (pat, flag) =
- toggle (Constr_matching.is_matching env Evd.empty pat (EConstr.of_constr constr)) flag
+ toggle (Constr_matching.is_matching env (Evd.from_env env) pat (EConstr.of_constr constr)) flag
in
let match_subtype (pat, flag) =
toggle
(Constr_matching.is_matching_appsubterm ~closed:false
- env Evd.empty pat (EConstr.of_constr constr)) flag
+ env (Evd.from_env env) pat (EConstr.of_constr constr)) flag
in
let match_module (mdl, flag) =
toggle (Libnames.is_dirpath_prefix_of mdl path) flag
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e1ce4e194..f347798c6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1651,7 +1651,9 @@ let vernac_check_may_eval ~atts redexp glopt rc =
let vernac_declare_reduction ~atts s r =
let local = make_locality atts.locality in
- declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r))
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r))
(* The same but avoiding the current goal context if any *)
let vernac_global_check c =