Proofview.Refine: remove the handle type, and simplify the API.

Now, usual function from Evarutil are used to define evars instead of the variants from Proofview.Refine.

The [update] primitive which tried to patch the difference between pretyping functions and the refine primitive is now replaced by the identity function.

5 files changed, 38 insertions, 70 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index cc380ed051..8cb50d77ff 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -959,16 +959,6 @@ end
 
 module Refine =
 struct
-  type handle = Evd.evar_map
-
-  let new_evar evd ?(main=false) env typ =
-    Evarutil.new_evar env evd ~principal:main typ
-
-  let new_evar_instance evd ctx typ inst =
-    Evarutil.new_evar_instance ctx evd typ inst
-
-  let fresh_constructor_instance evd env construct =
-    Evd.fresh_constructor_instance env evd construct
 
   let with_type evd env c t =
     let my_type = Retyping.get_type_of env evd c in
@@ -1018,8 +1008,6 @@ struct
     let f h = let (h, c) = f h in with_type h env c concl in
     refine ~unsafe f
   end
-
-  let update evd f = f evd
 end
 
 module NonLogical = Proofview_monad.NonLogical
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 671bd414ea..2dd470a970 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -433,36 +433,16 @@ end
     ill-typed terms without noticing. *)
 module Refine : sig
 
-  type handle
-  (** A handle to thread along in state-passing style. *)
-
-  val new_evar : handle -> ?main:bool ->
-    Environ.env -> Constr.types -> handle * Constr.t
-  (** Create a new hole that will be added to the goals to solve. *)
-
-  val new_evar_instance : handle -> Environ.named_context_val ->
-    Constr.types -> Constr.t list -> handle * Constr.t
-  (** Create a new hole with the given signature and instance. *)
-
-  val fresh_constructor_instance :
-    handle -> Environ.env -> Names.constructor -> handle * Constr.pconstructor
-  (** Creates a constructor with fresh universe variables. *)
-
-  val update : handle -> (Evd.evar_map -> Evd.evar_map * 'a) -> handle * 'a
-  (** [update h f] update the handle by applying [f] to the underlying evar map.
-      The [f] function must be monotonous, that is, for any evar map [evd],
-      [fst (f evd)] should be an extension of [evd]. New evars generated by [f]
-      are turned into goals. Use with care. *)
-
-  val refine : ?unsafe:bool -> (handle -> handle * Constr.t) -> unit tactic
-  (** Given a term with holes that have been generated through {!new_evar}, this
-      function fills the current hole with the given constr and creates goals
-      for all the holes in their generation order. Exceptions raised by the
-      function are caught. *)
-
-  val refine_casted : ?unsafe:bool -> (handle -> handle * Constr.t) -> unit tactic
-  (** Like {!refine} except the refined term is coerced to the conclusion of the
-      current goal. *)
+  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic
+  (** Given a term with holes that have been generated through
+      {!new_evar}, this function fills the current hole with the given
+      constr and creates goals for all the holes in their generation
+      order. The [evar_map] in the argument function is assumed to
+      only increase. Exceptions raised by the function are caught. *)
+
+  val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic
+(** Like {!refine} except the refined term is coerced to the conclusion of the
+    current goal. *)
 
 end
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 342e65cba7..e0995096fc 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -373,7 +373,7 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       Pretyping.ltac_idents = closure.Glob_term.idents;
     } in
     let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in
-    Proofview.Refine.refine ~unsafe:false (fun h -> Proofview.Refine.update h update) <*>
+    Proofview.Refine.refine ~unsafe:false update <*>
     Proofview.V82.tactic (reduce refine_red_flags refine_locs)
   end
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 0207b9b0f3..05184c8a28 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1501,7 +1501,7 @@ let new_refine (evd, c) =
     let evd = Evarconv.consider_remaining_unif_problems env evd in
     (evd, c)
   in
-  Proofview.Refine.refine_casted (fun h -> Proofview.Refine.update h update)
+  Proofview.Refine.refine_casted update
   end
 
 let assert_replacing id newt tac = 
@@ -1515,17 +1515,17 @@ let assert_replacing id newt tac =
           else decl :: nc')
         env ~init:[]
     in
-    Proofview.Refine.refine begin fun h ->
+    Proofview.Refine.refine begin fun sigma ->
       let env' = Environ.reset_with_named_context (val_of_named_context nc') env in
-      let h, ev = Proofview.Refine.new_evar h env' concl in
-      let h, ev' = Proofview.Refine.new_evar h env newt in
+      let sigma, ev = Evarutil.new_evar env' sigma concl in
+      let sigma, ev' = Evarutil.new_evar env sigma newt in
       let fold _ (n, b, t) inst =
         if Id.equal n id then ev' :: inst
         else mkVar n :: inst
       in
       let inst = fold_named_context fold env ~init:[] in
       let (e, args) = destEvar ev in
-      h, mkEvar (e, Array.of_list inst)
+      sigma, mkEvar (e, Array.of_list inst)
     end
   end in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
@@ -1547,10 +1547,10 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	| None, (undef, Some p, newt) ->
             Proofview.Goal.enter begin fun gl ->
             let env = Proofview.Goal.env gl in
-            let make h =
-              let (h, ()) = Proofview.Refine.update h (fun _ -> undef, ()) in
-              let (h, ev) = Proofview.Refine.new_evar h env newt in
-              h, mkApp (p, [| ev |])
+            let make sigma =
+              let (sigma, ()) = undef, () in
+              let (sigma, ev) = Evarutil.new_evar env sigma newt in
+              sigma, mkApp (p, [| ev |])
             in
             Proofview.Refine.refine make
             end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3d25e76073..1f8a57f07f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -133,9 +133,9 @@ let convert_concl ?(check=true) ty k =
       end else sigma in
     Tacticals.New.tclTHEN
       (Proofview.V82.tclEVARS sigma)
-      (Proofview.Refine.refine (fun h ->
-        let (h,x) = Proofview.Refine.new_evar h ~main:true env ty in
-        (h, if k == DEFAULTcast then x else mkCast(x,k,conclty))))
+      (Proofview.Refine.refine (fun sigma ->
+        let (sigma,x) = Evarutil.new_evar env sigma ~principal:true ty in
+        (sigma, if k == DEFAULTcast then x else mkCast(x,k,conclty))))
   end
 
 let convert_hyp ?(check=true) d =
@@ -145,7 +145,7 @@ let convert_hyp ?(check=true) d =
     let ty = Proofview.Goal.raw_concl gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
-    Proofview.Refine.refine (fun h -> Proofview.Refine.new_evar h ~main:true env ty)
+    Proofview.Refine.refine (fun sigma -> Evarutil.new_evar env sigma ~principal:true ty)
   end
 
 let convert_concl_no_check = convert_concl ~check:false
@@ -834,8 +834,8 @@ let cut c =
       (** Backward compat: normalize [c]. *)
       let c = local_strong whd_betaiota sigma c in
       Proofview.Refine.refine ~unsafe:true begin fun h ->
-        let (h, f) = Proofview.Refine.new_evar ~main:true h env (mkArrow c (Vars.lift 1 concl)) in
-        let (h, x) = Proofview.Refine.new_evar h env c in
+        let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
+        let (h, x) = Evarutil.new_evar env h c in
         let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
         (h, mkApp (f, [|x|]))
       end
@@ -1468,12 +1468,12 @@ let cut_and_apply c =
       | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
-        Proofview.Refine.refine begin fun h ->
+        Proofview.Refine.refine begin fun sigma ->
           let typ = mkProd (Anonymous, c2, concl) in
-          let (h, f) = Proofview.Refine.new_evar h env typ in
-          let (h, x) = Proofview.Refine.new_evar h env c1 in
+          let (sigma, f) = Evarutil.new_evar env sigma typ in
+          let (sigma, x) = Evarutil.new_evar env sigma c1 in
           let ans = mkApp (f, [|mkApp (c, [|x|])|]) in
-          (h, ans)
+          (sigma, ans)
         end
       | _ -> error "lapply needs a non-dependent product."
   end
@@ -1613,8 +1613,8 @@ let clear_body ids =
       check_is_type env concl msg
     in
     check_hyps <*> check_concl <*>
-    Proofview.Refine.refine ~unsafe:true begin fun h ->
-      Proofview.Refine.new_evar h env concl
+    Proofview.Refine.refine ~unsafe:true begin fun sigma ->
+      Evarutil.new_evar env sigma concl
     end
   end
 
@@ -2183,9 +2183,9 @@ let bring_hyps hyps =
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (instance_from_named_context hyps) in
-      Proofview.Refine.refine begin fun h ->
-        let (h, ev) = Proofview.Refine.new_evar h env newcl in
-        (h, (mkApp (ev, args)))
+      Proofview.Refine.refine begin fun sigma ->
+        let (sigma, ev) = Evarutil.new_evar env sigma newcl in
+        (sigma, (mkApp (ev, args)))
       end
     end
 
@@ -2295,9 +2295,9 @@ let new_generalize_gen_let lconstr =
 	0 lconstr ((concl, sigma), [])
     in
       Proofview.V82.tclEVARS sigma <*>
-	Proofview.Refine.refine begin fun h ->
-          let (h, ev) = Proofview.Refine.new_evar h env newcl in
-            (h, (applist (ev, args)))
+	Proofview.Refine.refine begin fun sigma ->
+          let (sigma, ev) = Evarutil.new_evar env sigma newcl in
+            (sigma, (applist (ev, args)))
 	end
   end