From 9f65b8bf9775dd571a806e10ac356b1b8f8ae2c5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 8 Oct 2018 02:14:07 +0200
Subject: Cleanup evar_extra: remove evar_info's store and add maps to evar_map

---
 proofs/clenv.ml    |  4 ++--
 proofs/clenvtac.ml |  4 ++--
 proofs/goal.ml     | 12 +++---------
 proofs/goal.mli    |  6 +-----
 proofs/logic.ml    |  4 ++--
 5 files changed, 10 insertions(+), 20 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 95e908c4dd..7ebc789aa5 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -608,8 +608,8 @@ let make_evar_clause env sigma ?len t =
     else match EConstr.kind sigma t with
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
-      let store = Typeclasses.set_resolvable Evd.Store.empty false in
-      let (sigma, ev) = new_evar ~store env sigma t1 in
+      let (sigma, ev) = new_evar env sigma t1 in
+      let sigma = Evd.set_resolvable_evar sigma (fst (destEvar sigma ev)) false in
       let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ba4cde6d67..929443a969 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -65,8 +65,8 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
 (** Use our own fast path, more informative than from Typeclasses *)
 let check_tc evd =
   let has_resolvable = ref false in
-  let check _ evi =
-    let res = Typeclasses.is_resolvable evi in
+  let check ev evi =
+    let res = Evd.is_resolvable_evar evd ev in
     if res then
       let () = has_resolvable := true in
       Typeclasses.is_class_evar evd evi
diff --git a/proofs/goal.ml b/proofs/goal.ml
index c14c0a8a77..6aff43f741 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -50,13 +50,8 @@ module V82 = struct
     let evi = Evd.find evars gl in
     evi.Evd.evar_concl
 
-  (* Access to ".evar_extra" *)
-  let extra evars gl =
-    let evi = Evd.find evars gl in
-    evi.Evd.evar_extra
-
   (* Old style mk_goal primitive *)
-  let mk_goal evars hyps concl extra =
+  let mk_goal evars hyps concl =
     (* A goal created that way will not be used by refine and will not
        be shelved. It must not appear as a future_goal, so the future
        goals are restored to their initial value after the evar is
@@ -67,11 +62,10 @@ module V82 = struct
 		Evd.evar_filter = Evd.Filter.identity;
 		Evd.evar_body = Evd.Evar_empty;
 		Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
-		Evd.evar_candidates = None;
-		Evd.evar_extra = extra }
+                Evd.evar_candidates = None }
     in
-    let evi = Typeclasses.mark_unresolvable evi in
     let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
+    let evars = Evd.set_resolvable_evar evars evk false in
     let evars = Evd.restore_future_goals evars prev_future_goals in
     let ctxt = Environ.named_context_of_val hyps in
     let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index a033d6daab..3b31cff8d7 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -39,16 +39,12 @@ module V82 : sig
   (* Access to ".evar_concl" *)
   val concl : Evd.evar_map -> goal -> EConstr.constr
 
-  (* Access to ".evar_extra" *)
-  val extra : Evd.evar_map -> goal -> Evd.Store.t
-
-  (* Old style mk_goal primitive, returns a new goal with corresponding 
+  (* Old style mk_goal primitive, returns a new goal with corresponding
        hypotheses and conclusion, together with a term which is precisely
        the evar corresponding to the goal, and an updated evar_map. *)
   val mk_goal : Evd.evar_map -> 
                          Environ.named_context_val ->
                          EConstr.constr ->
-                         Evd.Store.t ->
                          goal * EConstr.constr * Evd.evar_map
 
   (* Instantiates a goal with an open term *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 285240872e..254c93d0a2 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -350,7 +350,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = Goal.V82.env sigma goal in
   let hyps = Goal.V82.hyps sigma goal in
   let mk_goal hyps concl =
-    Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
+    Goal.V82.mk_goal sigma hyps concl
   in
     if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
       let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in
@@ -433,7 +433,7 @@ and mk_hdgoals sigma goal goalacc trm =
   let env = Goal.V82.env sigma goal in
   let hyps = Goal.V82.hyps sigma goal in
   let mk_goal hyps concl = 
-    Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+    Goal.V82.mk_goal sigma hyps concl in
   match kind trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-- 
cgit v1.2.3