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 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/firstorder/sequent.ml')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 4a93e01dca..435ca1986e 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
-- 
cgit v1.2.3