diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/library/declare.ml b/library/declare.ml index 9741ca9fa5..1bd7ad97e1 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -390,7 +390,8 @@ let library_part ref = let sp = Nametab.sp_of_global (Global.env ()) ref in let dir,_ = repr_path sp in match strength_of_global ref with - | DischargeAt (dp,n) -> extract_dirpath_prefix n dp + | DischargeAt (dp,n) -> + extract_dirpath_prefix n dp | NeverDischarge -> if is_dirpath_prefix_of dir (Lib.cwd ()) then (* Theorem/Lemma not yet (fully) discharged *) @@ -399,5 +400,3 @@ let library_part ref = (* Theorem/Lemma outside its outer section of definition *) dir | NotDeclare -> assert false - - |