diff options
| author | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
| commit | 8500216ac8df90b2afc0f5fd42d714cc87c6bde6 (patch) | |
| tree | 76a1ebe10646d2432f1539fb7ee9c6b0691ea221 /tactics | |
| parent | 9281bb33f2b9aa5d762f8b5b8b0159984b696efb (diff) | |
| parent | 8fafc201699e3d6c80e39bbadf2e6a5ba6425036 (diff) | |
Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/btermdn.ml | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/term_dnet.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index aca7f6c65e..bfee0422e7 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -28,7 +28,7 @@ type term_label = | SortLabel let compare_term_label t1 t2 = match t1, t2 with -| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2 +| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.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/hints.ml b/tactics/hints.ml index 43a450ea71..dce1a1bef6 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -288,7 +288,7 @@ let lookup_tacs sigma concl st se = let sl' = List.stable_sort pri_order_int l' in List.merge pri_order_int se.sentry_nopat sl' -module Constr_map = Map.Make(RefOrdered) +module Constr_map = Map.Make(GlobRef.Ordered) let is_transparent_gr (ids, csts) = function | VarRef id -> Id.Pred.mem id ids diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 8bdcc63215..03d2a17eee 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -100,7 +100,7 @@ struct | DRel, _ -> -1 | _, DRel -> 1 | DSort, DSort -> 0 | DSort, _ -> -1 | _, DSort -> 1 - | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2 + | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2 | DRef _, _ -> -1 | _, DRef _ -> 1 | DCtx (tl1, tr1), DCtx (tl2, tr2) |