aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/nbtermdn.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/nbtermdn.mli')
-rw-r--r--tactics/nbtermdn.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 8665cc705..350b53df7 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -34,5 +34,5 @@ val dnet_depth : int ref
val freeze : ('na,'a) t -> ('na,'a) frozen_t
val unfreeze : ('na,'a) frozen_t -> ('na,'a) t -> unit
val empty : ('na,'a) t -> unit
-val to2lists : ('na,'a) t -> ('na * (constr_pattern * 'a)) list *
+val to2lists : ('na,'a) t -> ('na * (constr_pattern * 'a)) list *
(global_reference option * 'a Btermdn.t) list