diff options
| author | Gaëtan Gilbert | 2019-07-03 10:12:04 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-03 17:05:29 +0200 |
| commit | 6e22817c6dab5043f1bdcbb1a1c8da281d4b3d7b (patch) | |
| tree | 94b89889210aa81e22208de97d90271e797a99be /vernac | |
| parent | bffe3e43a51420293960cc3c32845687bdee5f9b (diff) | |
declare_variable: path is always Lib.cwd()
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comAssumption.ml | 2 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 6 |
3 files changed, 5 insertions, 5 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 520df1c21e..c561d4a2a4 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -51,7 +51,7 @@ match scope with | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs in let kind = Decls.IsAssumption kind in - let decl = Lib.cwd(), SectionLocalAssum {typ; univs; poly; impl} in + let decl = SectionLocalAssum {typ; univs; poly; impl} in let () = declare_variable ~name ~kind decl in let () = assumption_message name in let r = VarRef name in 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 -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d6ee0b96f2..ea735dd7f9 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -266,7 +266,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i | Monomorphic_entry univs -> univs in let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in - let () = Declare.declare_variable ~name ~kind (Lib.cwd(),c) in + let () = Declare.declare_variable ~name ~kind c in (VarRef name,impargs) | Global local -> let kind = Decls.(IsAssumption Conjectural) in @@ -289,7 +289,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i | Discharge -> let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in let c = Declare.SectionLocalDef const in - let () = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in + let () = Declare.declare_variable ~name ~kind c in (VarRef name,impargs) | Global local -> let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in @@ -499,7 +499,7 @@ let finish_proved env sigma idopt po info = let r = match scope with | Discharge -> let c = Declare.SectionLocalDef const in - let () = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in + let () = Declare.declare_variable ~name ~kind c in let () = if should_suggest then Proof_using.suggest_variable (Global.env ()) name in |