Merge PR #7359: Reduce usage of evar_map references

4 files changed, 16 insertions, 15 deletions

diff --git a/proofs/refine.ml b/proofs/refine.ml
index 5a2d82977e..b64e7a2e5e 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -30,26 +30,19 @@ let typecheck_evar ev env sigma =
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
     let t = NamedDecl.get_type decl in
-    let evdref = ref sigma in
-    let _ = Typing.e_sort_of env evdref t in
-    let () = match decl with
-    | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+    let sigma, _ = Typing.sort_of env sigma t in
+    let sigma = match decl with
+    | LocalAssum _ -> sigma
+    | LocalDef (_,body,_) -> Typing.check env sigma body t
     in
-    (!evdref, EConstr.push_named decl env)
+    (sigma, EConstr.push_named decl env)
   in
   let (common, changed) = extract_prefix env info in
   let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
-  let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
-  !evdref
-
-let typecheck_proof c concl env sigma =
-  let evdref = ref sigma in
-  let () = Typing.e_check env evdref c concl in
-  !evdref
+  let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
+  sigma
 
 let (pr_constrv,pr_constr) =
   Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
@@ -93,7 +86,7 @@ let generic_refine ~typecheck f gl =
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
   (** Check that the refined term is typesafe *)
-  let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
+  let sigma = if typecheck then Typing.check env sigma c concl else sigma in
   (** Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5cd703a25c..0f83e16ec8 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -23,9 +23,12 @@ val pf_env  : goal sigma -> Environ.env
 val pf_hyps : goal sigma -> named_context
 
 val unpackage : 'a sigma -> evar_map ref * 'a
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val repackage : evar_map ref -> 'a -> 'a sigma
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val apply_sig_tac :
   evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 
 val refiner : rule -> tactic
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 1889054f86..c1d69dfc54 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -33,9 +33,11 @@ let re_sig it  gc = { it = it; sigma = gc; }
 type 'a sigma   = 'a Evd.sigma;;
 type tactic     = Proof_type.tactic;;
 
+[@@@ocaml.warning "-3"]
 let unpackage = Refiner.unpackage
 let repackage = Refiner.repackage
 let apply_sig_tac = Refiner.apply_sig_tac
+[@@@ocaml.warning "+3"]
 
 let sig_it   = Refiner.sig_it
 let project  = Refiner.project
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index de96f85104..31496fb3d5 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -30,9 +30,12 @@ val project : goal sigma -> evar_map
 val re_sig : 'a -> evar_map -> 'a sigma
 
 val unpackage : 'a sigma -> evar_map ref * 'a
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val repackage : evar_map ref -> 'a -> 'a sigma
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 val apply_sig_tac :
   evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list)
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env