diff options
Diffstat (limited to 'tactics/termdn.mli')
| -rw-r--r-- | tactics/termdn.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/termdn.mli b/tactics/termdn.mli index 6a6dfe340..6e1bdd87c 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -11,6 +11,7 @@ (*i*) open Term open Pattern +open Libnames (*i*) (* Discrimination nets of terms. *) @@ -44,8 +45,8 @@ val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit (* These are for Nbtermdn *) val constr_pat_discr : - constr_pattern -> (constr_label * constr_pattern list) option + constr_pattern -> (global_reference * constr_pattern list) option val constr_val_discr : - constr -> (constr_label * constr list) option + constr -> (global_reference * constr list) option (*i*) |