From ba372c87f7a21cbc8bfcd4495bd59a04a63f7281 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 10 Oct 2014 17:08:42 +0200 Subject: Expose Proofview.Refine.with_type in the API. --- proofs/proofview.mli | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'proofs/proofview.mli') 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 -- cgit v1.2.3