diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-07 17:41:10 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-07 17:41:10 +0000 |
| commit | 22cb4d34d7f67eb98c737b076a4ecbbf800bdc55 (patch) | |
| tree | 9a238c0c4919245db39f805056754b1798e94357 /tactics/termdn.mli | |
| parent | e2363aafc80d9a8efaf9c13bbf9e4e5bb0f4eb10 (diff) | |
The type Pattern.constr_label was isomorphic to Libnames.global_reference.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6427 85f007b7-540e-0410-9357-904b9bb8a0f7
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*) |