diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-12 17:46:18 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-24 17:35:20 +0200 |
| commit | d5d80dfc0f773fd6381ee4efefc74804d103fe4e (patch) | |
| tree | 73be62f93b8716b5b69fadf705a91e106dadec17 /proofs/logic.ml | |
| parent | f5f4bb97634f4fac3dec766db27af994e745d749 (diff) | |
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index aa0b9bac6..39dff4aca 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -213,7 +213,7 @@ let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom | d :: right -> - let hyp,_,typ = to_tuple d in + let hyp = get_id d in if Id.equal hyp hfrom then (left,right,d, toleft || move_location_eq hto MoveLast) else @@ -489,15 +489,16 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp check sign sigma d = - let id,b,bt = to_tuple d in + let id = get_id d in + let b = get_value d in let env = Global.env() in let reorder = ref [] in let sign' = apply_to_hyp check sign id (fun _ d' _ -> - let _,c,ct = to_tuple d' in + let c = get_value d' in let env = Global.env_of_context sign in - if check && not (is_conv env sigma bt ct) then + if check && not (is_conv env sigma (get_type d) (get_type d')) then errorlabstrm "Logic.convert_hyp" (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then |