diff options
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 40 |
1 files changed, 10 insertions, 30 deletions
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 |