aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-03 17:44:34 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-25 14:55:49 +0200
commitdfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch)
tree33fdd7c2eb44e54e7777e2d074127b129c5385ac /plugins
parentd2533da244f770261478ae829167cb3a8ad38038 (diff)
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
Diffstat (limited to 'plugins')
-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
11 files changed, 44 insertions, 25 deletions
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()