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/proofview.ml | |
| parent | 27632acf63d638e050d26b7fc107a55e13323a0c (diff) | |
Expose Proofview.Refine.with_type in the API.
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 4 |
1 files changed, 2 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 |