diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/library/declare.ml b/library/declare.ml index 6b2f9a6ae..fc80cfda9 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -35,10 +35,7 @@ open Safe_typing (useful only for persistent constructions), is the length of the section part in [dir] *) -type strength = - | NotDeclare - | DischargeAt of dir_path * int - | NeverDischarge +open Nametab let depth_of_strength = function | DischargeAt (sp',n) -> n |