diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-17 20:50:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-17 22:30:43 +0200 |
| commit | dadd4003b6607ccc103658f842b5efbd6d8ab57f (patch) | |
| tree | 6f8b1b8ba71681b06b4a74ddeee76d02a3ef09dd /proofs | |
| parent | 43343c1f79d9f373104ae5174baf41e2257e2b8d (diff) | |
Removing some compatibility layers in Tactics.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 36ae5554f..fd8a70c65 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -77,10 +77,10 @@ let with_check = Flags.with_option check (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp sign id f = +let apply_to_hyp check sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if !check then error_no_such_hypothesis id + if check then error_no_such_hypothesis id else sign let check_typability env sigma c = @@ -493,7 +493,7 @@ let convert_hyp check sign sigma d = let env = Global.env() in let reorder = ref [] in let sign' = - apply_to_hyp sign id + apply_to_hyp check sign id (fun _ d' _ -> let _,c,ct = to_tuple d' in let env = Global.env_of_context sign in |