diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-10 17:08:42 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:23:29 +0200 |
| commit | ba372c87f7a21cbc8bfcd4495bd59a04a63f7281 (patch) | |
| tree | cd2dfaf854506616560806206aea8982c905032b /proofs/proofview.mli | |
| parent | 27632acf63d638e050d26b7fc107a55e13323a0c (diff) | |
Expose Proofview.Refine.with_type in the API.
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2dd470a97..90a1b9fba 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -433,6 +433,11 @@ end ill-typed terms without noticing. *) module Refine : sig + val with_type : Environ.env -> Evd.evar_map -> + Term.constr -> Term.types -> Evd.evar_map * Term.constr + (** [with_type env sigma c t] ensures that [c] is of type [t] + inserting a coercion if needed. *) + 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 |