diff options
Diffstat (limited to 'tactics/btermdn.ml')
| -rw-r--r-- | tactics/btermdn.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index a476381b17..70819e9550 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -29,7 +29,7 @@ type term_label = let compare_term_label t1 t2 = match t1, t2 with | GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2 -| _ -> Pervasives.compare t1 t2 (** OK *) +| _ -> pervasives_compare t1 t2 (** OK *) type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything |