From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Mon, 29 May 2017 11:02:06 +0200 Subject: Remove (useless) aliases from the API. --- plugins/firstorder/sequent.ml | 7 +++---- plugins/firstorder/sequent.mli | 6 +++--- plugins/firstorder/unify.ml | 4 ++-- 3 files changed, 8 insertions(+), 9 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 4a93e01dc..435ca1986 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,7 +7,6 @@ (************************************************************************) open API -open Term open EConstr open CErrors open Util @@ -58,11 +57,11 @@ end module OrderedConstr= struct - type t=Constr.t - let compare=constr_ord + type t=Term.constr + let compare=Term.compare end -type h_item = global_reference * (int*Constr.t) option +type h_item = global_reference * (int*Term.constr) option module Hitem= struct diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index c43a91cee..e24eca7cb 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -11,11 +11,11 @@ open EConstr open Formula open Globnames -module OrderedConstr: Set.OrderedType with type t=Constr.t +module OrderedConstr: Set.OrderedType with type t=Term.constr -module CM: CSig.MapS with type key=Constr.t +module CM: CSig.MapS with type key=Term.constr -type h_item = global_reference * (int*Constr.t) option +type h_item = global_reference * (int*Term.constr) option module History: Set.S with type elt = h_item diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 24fd8dd88..e1adebe8d 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -55,12 +55,12 @@ let unif evd t1 t2= | Meta i,_ -> let t=subst_meta !sigma nt2 in if Int.Set.is_empty (free_rels evd t) && - not (occur_term evd (EConstr.mkMeta i) t) then + not (dependent evd (EConstr.mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in if Int.Set.is_empty (free_rels evd t) && - not (occur_term evd (EConstr.mkMeta i) t) then + not (dependent evd (EConstr.mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige -- cgit v1.2.3