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 /plugins/omega | |
| parent | f5f4bb97634f4fac3dec766db27af994e745d749 (diff) | |
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d625e3076..c5c44ef20 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1697,8 +1697,8 @@ let destructure_hyps = let rec loop = function | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) | decl::lit -> - let (i,_,t) = to_tuple decl in - begin try match destructurate_prop t with + let i = get_id decl in + begin try match destructurate_prop (get_type decl) with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> |