aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/declare.ml')
-rw-r--r--library/declare.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 84cc2e575..2383ca304 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -17,12 +17,12 @@ open Impargs
open Indrec
type strength =
- | DischargeAt of section_path
+ | DischargeAt of dir_path
| NeverDischarge
let make_strength = function
| [] -> NeverDischarge
- | l -> DischargeAt (sp_of_wd l)
+ | l -> DischargeAt l
let make_strength_0 () = make_strength (Lib.cwd())