Proofview.Goal.sigma returns an indexed evarmap.

5 files changed, 13 insertions, 7 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 65bd325362..894b290f14 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -121,7 +121,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Tacmach.New.pf_env gl in
     let n = Tacmach.New.pf_nf_concl gl in
-    let evd = clear_metas (Proofview.Goal.sigma gl) in
+    let evd = clear_metas (Tacmach.New.project gl) in
     try
       let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 826b4772a0..bded518e78 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -921,7 +921,7 @@ module Goal = struct
   let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t)
 
   let env { env=env } = env
-  let sigma { sigma=sigma } = sigma
+  let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma
   let hyps { env=env } = Environ.named_context env
   let concl { concl=concl } = concl
   let extra { sigma=sigma; self=self } = Goal.V82.extra sigma self
@@ -1061,6 +1061,7 @@ struct
 
   let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl ->
     let sigma = Goal.sigma gl in
+    let sigma = Sigma.to_evar_map sigma in
     let env = Goal.env gl in
     let concl = Goal.concl gl in
     (** Save the [future_goals] state to restore them after the
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 5c97ada344..0b6c147f92 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -444,7 +444,7 @@ module Goal : sig
   val concl : ([ `NF ], 'r) t -> Term.constr
   val hyps : ([ `NF ], 'r) t -> Context.named_context
   val env : ('a, 'r) t -> Environ.env
-  val sigma : ('a, 'r) t -> Evd.evar_map
+  val sigma : ('a, 'r) t -> 'r Sigma.t
   val extra : ('a, 'r) t -> Evd.Store.t
 
   (** Returns the goal's conclusion even if the goal is not
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8af28b6ab1..57c60cbeed 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -158,11 +158,15 @@ let pr_glls glls =
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New = struct
 
+  let project gl =
+    let sigma = Proofview.Goal.sigma gl in
+    Sigma.to_evar_map sigma
+
   let pf_apply f gl =
-    f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)
+    f (Proofview.Goal.env gl) (project gl)
 
   let of_old f gl =
-    f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl }
+    f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
 
   let pf_global id gl =
     (** We only check for the existence of an [id] in [hyps] *)
@@ -216,7 +220,7 @@ module New = struct
     (** We normalize the conclusion just after *)
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = project gl in
     nf_evar sigma concl
 
   let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
@@ -235,6 +239,6 @@ module New = struct
   let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
   let pf_compute gl t = pf_apply compute gl t
 
-  let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t
+  let pf_nf_evar gl t = nf_evar (project gl) t
 
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 3ed6a2eeb1..c45fd250cb 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -111,6 +111,7 @@ module New : sig
   (** FIXME: encapsulate the level in an existential type. *)
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a
 
+  val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
   val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
   val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types