diff options
Diffstat (limited to 'tactics/termdn.ml')
| -rw-r--r-- | tactics/termdn.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 0e7009113..ce7ac29f1 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -14,7 +14,7 @@ open Term open Pattern open Patternops open Glob_term -open Libnames +open Globnames open Nametab (* Discrimination nets of terms. |