aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareDef.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/declareDef.ml')
-rw-r--r--vernac/declareDef.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 2aa96fa8ed..69338c0ba6 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -49,7 +49,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
let gr = match scope with
| Discharge ->
let () =
- declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce)
+ declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce)
in
VarRef name
| Global local ->