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 | |
| parent | f5f4bb97634f4fac3dec766db27af994e745d749 (diff) | |
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 9 | ||||
| -rw-r--r-- | proofs/proof_using.ml | 10 |
2 files changed, 11 insertions, 8 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 diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index caa9b328a..5b24a1fb2 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -35,12 +35,14 @@ let in_nameset = let rec close_fwd e s = let s' = List.fold_left (fun s decl -> - let (id,b,ty) = Context.Named.Declaration.to_tuple decl in - let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in - let vty = global_vars_set e ty in + let vb = match decl with + | LocalAssum _ -> Id.Set.empty + | LocalDef (_,b,_) -> global_vars_set e b + in + let vty = global_vars_set e (get_type decl) in let vbty = Id.Set.union vb vty in if Id.Set.exists (fun v -> Id.Set.mem v s) vbty - then Id.Set.add id (Id.Set.union s vbty) else s) + then Id.Set.add (get_id decl) (Id.Set.union s vbty) else s) s (named_context e) in if Id.Set.equal s s' then s else close_fwd e s' |