Merge remote-tracking branch 'upstream/trunk' into trunk

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index a81b8944c9..15d0f5f37c 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)