diff options
Diffstat (limited to 'plugins/omega/coq_omega.ml')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 0bf30e7fd..1afc6500b 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -open Errors +open CErrors open Util open Names open Nameops @@ -30,6 +30,7 @@ open Misctypes open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -911,7 +912,7 @@ let rec transform p t = try let v,th,_ = find_constr t' in [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> let v = new_identifier_var () and th = new_identifier () in hide_constr t' v th isnat; @@ -951,7 +952,7 @@ let rec transform p t = end | Kapp((Zpos|Zneg|Z0),_) -> (try ([],Oz(recognize_number t)) - with e when Errors.noncritical e -> default false t) + with e when CErrors.noncritical e -> default false t) | Kvar s -> [],Oatom s | Kapp(Zopp,[t]) -> let tac,t' = transform (P_APP 1 :: p) t in @@ -1697,8 +1698,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 = NamedDecl.get_id decl in + begin try match destructurate_prop (NamedDecl.get_type decl) with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> @@ -1808,13 +1809,13 @@ let destructure_hyps = match destructurate_type (pf_nf typ) with | Kapp(Nat,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) - decl)) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + decl)) (loop lit)) | Kapp(Z,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) - decl)) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + decl)) (loop lit)) | _ -> loop lit end |