diff options
Diffstat (limited to 'plugins/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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) |