diff options
| author | Pierre-Marie Pédrot | 2020-09-22 18:36:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:21:14 +0200 |
| commit | 0a46af10ffc38726207bca952775102d48ad3b15 (patch) | |
| tree | 03ca56bb87e50a5d33c29183f74058fc99302735 /tactics | |
| parent | 0590764209dcb8540b5292aca38fe2df38b90ab9 (diff) | |
Rename the GlobRef comparison modules following the standard pattern.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/btermdn.ml | 2 | ||||
| -rw-r--r-- | tactics/term_dnet.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index f721e9956b..af0ca22868 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -27,7 +27,7 @@ type term_label = | SortLabel let compare_term_label t1 t2 = match t1, t2 with -| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2 +| GRLabel gr1, GRLabel gr2 -> GlobRef.CanOrd.compare gr1 gr2 | _ -> pervasives_compare t1 t2 (** OK *) type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 3bcd235b41..fee9dd1b96 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -107,7 +107,7 @@ struct | DRel, _ -> -1 | _, DRel -> 1 | DSort, DSort -> 0 | DSort, _ -> -1 | _, DSort -> 1 - | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2 + | DRef gr1, DRef gr2 -> GlobRef.CanOrd.compare gr1 gr2 | DRef _, _ -> -1 | _, DRef _ -> 1 | DCtx (tl1, tr1), DCtx (tl2, tr2) |