Cleanup evar_extra: remove evar_info's store and add maps to evar_map

3 files changed, 40 insertions, 54 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9bd406e14d..f075e5e44a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -513,12 +513,12 @@ let top_sort evm undefs =
 
 let evars_to_goals p evm =
   let goals = ref Evar.Map.empty in
-  let map ev evi =
-    let evi, goal = p evm ev evi in
+  let fold ev evi evm =
+    let evm, goal = p evm ev evi in
     let () = if goal then goals := Evar.Map.add ev evi !goals in
-    evi
+    evm
   in
-  let evm = Evd.raw_map_undefined map evm in
+  let evm = Evd.fold_undefined fold evm evm in
   if Evar.Map.is_empty !goals then None
   else Some (!goals, evm)
 
@@ -643,10 +643,7 @@ module Search = struct
 
   let mark_unresolvables sigma goals =
     List.fold_left
-      (fun sigma gl ->
-        let evi = Evd.find_undefined sigma gl in
-	let evi' = Typeclasses.mark_unresolvable evi in
-	Evd.add sigma gl evi')
+      (fun sigma gl -> Evd.set_resolvable_evar sigma gl false)
       sigma goals
 
   (** The general hint application tactic.
@@ -1019,7 +1016,7 @@ let deps_of_constraints cstrs evm p =
 let evar_dependencies pred evm p =
   Evd.fold_undefined
     (fun ev evi _ ->
-      if Typeclasses.is_resolvable evi && pred evm ev evi then
+      if Evd.is_resolvable_evar evm ev && pred evm ev evi then
         let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
         in Intpart.union_set evars p
       else ())
@@ -1036,7 +1033,7 @@ let split_evars pred evm =
 let is_inference_forced p evd ev =
   try
     let evi = Evd.find_undefined evd ev in
-    if Typeclasses.is_resolvable evi && snd (p ev evi)
+    if Evd.is_resolvable_evar evd ev && snd (p ev evi)
     then
       let (loc, k) = evar_source ev evd in
       match k with
@@ -1076,13 +1073,13 @@ let error_unresolvable env comp evd =
 let select_and_update_evars p oevd in_comp evd ev evi =
   assert (evi.evar_body == Evar_empty);
   try
-    let oevi = Evd.find_undefined oevd ev in
-    if Typeclasses.is_resolvable oevi then
-      Typeclasses.mark_unresolvable evi,
+    let _ = Evd.find_undefined oevd ev in
+    if Evd.is_resolvable_evar oevd ev then
+      Evd.set_resolvable_evar evd ev false,
       (in_comp ev && p evd ev evi)
-    else evi, false
+    else evd, false
   with Not_found ->
-    Typeclasses.mark_unresolvable evi, p evd ev evi
+    Evd.set_resolvable_evar evd ev false, p evd ev evi
 
 (** Do we still have unresolved evars that should be resolved ? *)
 
@@ -1095,17 +1092,17 @@ let has_undefined p oevd evd =
     just for this call to resolution. *)
 
 let revert_resolvability oevd evd =
-  let map ev evi =
+  let fold ev _evi evd =
     try
-      if not (Typeclasses.is_resolvable evi) then
-        let evi' = Evd.find_undefined oevd ev in
-        if Typeclasses.is_resolvable evi' then
-          Typeclasses.mark_resolvable evi
-        else evi
-      else evi
-    with Not_found -> evi
+      if not (Evd.is_resolvable_evar evd ev) then
+        let _evi' = Evd.find_undefined oevd ev in
+        if Evd.is_resolvable_evar oevd ev then
+          Evd.set_resolvable_evar evd ev true
+        else evd
+      else evd
+    with Not_found -> evd
   in
-  Evd.raw_map_undefined map evd
+  Evd.fold_undefined fold evd evd
 
 exception Unresolved
 
@@ -1161,8 +1158,7 @@ let _ =
 let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
   let (term, sigma) = Hints.wrap_hint_warning_fun env sigma begin fun sigma ->
   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
+  let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl in
   let (ev, _) = destEvar sigma t in
   let gls = { it = gl ; sigma = sigma; } in
   let hints = searchtable_map typeclasses_db in
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index f2bc679aac..6388aa2c33 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -72,11 +72,10 @@ let choose_noteq eqonleft =
 let generalize_right mk typ c1 c2 =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let store = Proofview.Goal.extra gl in
   Refine.refine ~typecheck:false begin fun sigma ->
     let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in
     let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
-    let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
+    let (sigma, x) = Evarutil.new_evar env sigma ~principal:true newconcl in
     (sigma, mkApp (x, [|c2|]))
   end
   end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 18ddc9318d..a6a104ccca 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -117,14 +117,14 @@ let _ =
 
 (** This tactic creates a partial proof realizing the introduction rule, but
     does not check anything. *)
-let unsafe_intro env store decl b =
+let unsafe_intro env decl b =
   Refine.refine ~typecheck:false begin fun sigma ->
     let ctx = named_context_val env in
     let nctx = push_named_context_val decl ctx in
     let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
-    let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+    let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ninst in
     (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev)
   end
 
@@ -133,7 +133,6 @@ let introduction id =
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let hyps = named_context_val (Proofview.Goal.env gl) in
-    let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
     let () = if mem_named_context_val id hyps then
       user_err ~hdr:"Tactics.introduction"
@@ -141,8 +140,8 @@ let introduction id =
     in
     let open Context.Named.Declaration in
     match EConstr.kind sigma concl with
-    | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
-    | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
+    | Prod (_, t, b) -> unsafe_intro env (LocalAssum (id, t)) b
+    | LetIn (_, c, t, b) -> unsafe_intro env (LocalDef (id, c, t)) b
     | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
   end
 
@@ -152,7 +151,6 @@ let error msg = CErrors.user_err Pp.(str msg)
 let convert_concl ?(check=true) ty k =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let store = Proofview.Goal.extra gl in
     let conclty = Proofview.Goal.concl gl in
     Refine.refine ~typecheck:false begin fun sigma ->
       let sigma =
@@ -162,7 +160,7 @@ let convert_concl ?(check=true) ty k =
           | None -> error "Not convertible."
           | Some sigma -> sigma
         end else sigma in
-      let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
+      let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in
       let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
       (sigma, ans)
     end
@@ -173,11 +171,10 @@ let convert_hyp ?(check=true) d =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.concl gl in
-    let store = Proofview.Goal.extra gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
     Refine.refine ~typecheck:false begin fun sigma ->
-      Evarutil.new_evar env sigma ~principal:true ~store ty
+      Evarutil.new_evar env sigma ~principal:true ty
     end
   end
 
@@ -284,12 +281,11 @@ let move_hyp id dest =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.concl gl in
-    let store = Proofview.Goal.extra gl in
     let sign = named_context_val env in
     let sign' = move_hyp_in_named_context env sigma id dest sign in
     let env = reset_with_named_context sign' env in
     Refine.refine ~typecheck:false begin fun sigma ->
-      Evarutil.new_evar env sigma ~principal:true ~store ty
+      Evarutil.new_evar env sigma ~principal:true ty
     end
   end
 
@@ -313,7 +309,6 @@ let rename_hyp repl =
     Proofview.Goal.enter begin fun gl ->
       let hyps = Proofview.Goal.hyps gl in
       let concl = Proofview.Goal.concl gl in
-      let store = Proofview.Goal.extra gl in
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
       (** Check that we do not mess variables *)
@@ -344,7 +339,7 @@ let rename_hyp repl =
       let nctx = val_of_named_context nhyps in
       let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
       Refine.refine ~typecheck:false begin fun sigma ->
-        Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
+        Evarutil.new_evar_instance nctx sigma nconcl ~principal:true instance
       end
     end
 
@@ -445,7 +440,6 @@ let internal_cut_gen ?(check=true) dir replace id t =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
-    let store = Proofview.Goal.extra gl in
     let sign = named_context_val env in
     let sign',t,concl,sigma =
       if replace then
@@ -464,10 +458,10 @@ let internal_cut_gen ?(check=true) dir replace id t =
         let (sigma,ev,ev') =
           if dir then
             let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
-            let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+            let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
             (sigma,ev,ev')
           else
-            let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+            let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
             let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
             (sigma,ev,ev') in
         let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in
@@ -2102,11 +2096,10 @@ let keep hyps =
 let apply_type ~typecheck newcl args =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let store = Proofview.Goal.extra gl in
     Refine.refine ~typecheck begin fun sigma ->
       let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in
       let (sigma, ev) =
-        Evarutil.new_evar env sigma ~principal:true ~store newcl in
+        Evarutil.new_evar env sigma ~principal:true newcl in
       (sigma, applist (ev, args))
     end
   end
@@ -2120,13 +2113,12 @@ let bring_hyps hyps =
   else
     Proofview.Goal.enter begin fun gl ->
       let env = Proofview.Goal.env gl in
-      let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
       Refine.refine ~typecheck:false begin fun sigma ->
         let (sigma, ev) =
-          Evarutil.new_evar env sigma ~principal:true ~store newcl in
+          Evarutil.new_evar env sigma ~principal:true newcl in
         (sigma, mkApp (ev, args))
       end
     end
@@ -2668,7 +2660,7 @@ let mk_eq_name env id {CAst.loc;v=ido} =
 
 (* unsafe *)
 
-let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
+let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty =
   let open Context.Named.Declaration in
   let t = match ty with Some t -> t | _ -> typ_of env sigma c in
   let decl = if dep then LocalDef (id,c,t)
@@ -2683,11 +2675,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
       let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
-      let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+      let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
       (sigma, mkNamedLetIn id c t (mkNamedLetIn heq refl eq x))
   | None ->
       let newenv = insert_before [decl] lastlhyp env in
-      let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+      let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
       (sigma, mkNamedLetIn id c t x)
 
 let pose_tac na c =
@@ -4431,7 +4423,6 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
   let ccl = Proofview.Goal.concl gl in
-  let store = Proofview.Goal.extra gl in
   let check = check_enough_applied env sigma elim in
   let (sigma', c) = use_bindings env sigma elim false (c0,lbind) t0 in
   let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in
@@ -4457,7 +4448,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
           let b = not with_evars && with_eq != None in
           let (sigma, c) = use_bindings env sigma elim b (c0,lbind) t0 in
           let t = Retyping.get_type_of env sigma c in
-          mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t)
+          mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t)
         end;
         if with_evars then Proofview.shelve_unifiable else guard_no_unifiable;
         if is_arg_pure_hyp
@@ -4478,7 +4469,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       let tac =
       Tacticals.New.tclTHENLIST [
         Refine.refine ~typecheck:false begin fun sigma ->
-          mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
+          mkletin_goal env sigma with_eq true (id,lastlhyp,ccl,c) None
         end;
         (tac inhyps)
       ]