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.

2 files changed, 10 insertions, 42 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index cc380ed05..8cb50d77f 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 671bd414e..2dd470a97 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