From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 plugins/quote/quote.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index a81b8944c..15d0f5f37 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -169,8 +169,8 @@ exchange ?1 and ?2 in the example above)
 
 module ConstrSet = Set.Make(
   struct
-    type t = Constr.constr
-    let compare = constr_ord
+    type t = Term.constr
+    let compare = Term.compare
   end)
 
 type inversion_scheme = {
@@ -387,7 +387,7 @@ let rec sort_subterm gl l =
     | h::t -> insert h (sort_subterm gl t)
 
 module Constrhash = Hashtbl.Make
-  (struct type t = Constr.constr
+  (struct type t = Term.constr
 	  let equal = Term.eq_constr
 	  let hash = Term.hash_constr
    end)
-- 
cgit v1.2.3