diff options
| author | Arnaud Spiwack | 2014-10-10 17:08:42 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-16 10:23:29 +0200 |
| commit | ba372c87f7a21cbc8bfcd4495bd59a04a63f7281 (patch) | |
| tree | cd2dfaf854506616560806206aea8982c905032b /proofs | |
| parent | 27632acf63d638e050d26b7fc107a55e13323a0c (diff) | |
Expose Proofview.Refine.with_type in the API.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 4 | ||||
| -rw-r--r-- | proofs/proofview.mli | 5 |
2 files changed, 7 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 8cb50d77ff..9110cb4f1e 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -960,7 +960,7 @@ end module Refine = struct - let with_type evd env c t = + let with_type env evd c t = let my_type = Retyping.get_type_of env evd c in let j = Environ.make_judge c my_type in let (evd,j') = @@ -1005,7 +1005,7 @@ struct let refine_casted ?(unsafe = false) f = Goal.enter begin fun gl -> let concl = Goal.concl gl in let env = Goal.env gl in - let f h = let (h, c) = f h in with_type h env c concl in + let f h = let (h, c) = f h in with_type env h c concl in refine ~unsafe f end end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2dd470a970..90a1b9fba9 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 |