diff options
| -rw-r--r-- | library/declare.ml | 6 | ||||
| -rw-r--r-- | library/declare.mli | 2 | ||||
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | library/lib.mli | 1 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 17 |
5 files changed, 20 insertions, 10 deletions
diff --git a/library/declare.ml b/library/declare.ml index 53a6ef83f..7bede5758 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -172,7 +172,7 @@ let cache_constant (sp,(cdt,stre,op)) = Nametab.push sp (ConstRef sp); (match stre with (* Remark & Fact outside their scope aren't visible without qualif *) - | DischargeAt sp when not (is_dirpath_prefix_of sp (Lib.cwd ())) -> () + | DischargeAt sp' when not (is_dirpath_prefix_of sp' (Lib.cwd ())) -> () (* Theorem, Lemma & Definition are accessible from the base name *) | NeverDischarge| DischargeAt _ -> Nametab.push_short_name sp (ConstRef sp) | NotDeclare -> assert false); @@ -219,6 +219,10 @@ let declare_constant id cd = if is_implicit_args() then declare_constant_implicits sp; sp +let redeclare_constant sp cd = + add_absolutely_named_lead sp (in_constant cd); + if is_implicit_args() then declare_constant_implicits sp + (* Inductives. *) diff --git a/library/declare.mli b/library/declare.mli index e17be37e3..08c45f462 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -52,6 +52,8 @@ type constant_declaration = constant_declaration_type * strength * opacity the full path of the declaration *) val declare_constant : identifier -> constant_declaration -> constant_path +val redeclare_constant : constant_path -> constant_declaration -> unit + val declare_parameter : identifier -> constr -> constant_path (* [declare_mind me] declares a block of inductive types with diff --git a/library/lib.ml b/library/lib.ml index 5995a9600..94cba5e0c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -95,6 +95,10 @@ let add_anonymous_entry node = add_entry sp node; sp +let add_absolutely_named_lead sp obj = + cache_object (sp,obj); + add_entry sp (Leaf obj) + let add_leaf id kind obj = let sp = make_path id kind in cache_object (sp,obj); diff --git a/library/lib.mli b/library/lib.mli index 4c802a0f8..27fec78bf 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -34,6 +34,7 @@ and library_segment = library_entry list current list of operations (most recent ones coming first). *) val add_leaf : identifier -> path_kind -> obj -> section_path +val add_absolutely_named_lead : section_path -> obj -> unit val add_anonymous_leaf : obj -> unit val add_frozen_state : unit -> unit diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index a9c1273e8..730817bf3 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -164,7 +164,7 @@ type opacity = bool type discharge_operation = | Variable of identifier * section_variable_entry * strength * bool * bool | Parameter of identifier * constr * bool - | Constant of identifier * recipe * strength * opacity * bool + | Constant of section_path * recipe * strength * opacity * bool | Inductive of mutual_inductive_entry * bool | Class of cl_typ * cl_info_typ | Struc of inductive_path * (unit -> struc_typ) @@ -216,9 +216,10 @@ let process_object oldenv dir sec_sp else *) let cb = Environ.lookup_constant sp oldenv in - let spid = basename sp in let imp = is_implicit_constant sp in - let newsp = recalc_sp dir sp in + let newsp = match stre with + | DischargeAt d when not (is_dirpath_prefix_of d dir) -> sp + | _ -> recalc_sp dir sp in let mods = let modl = build_abstract_list cb.const_hyps ids_to_discard in [ (sp, DO_ABSTRACT(newsp,modl)) ] @@ -226,7 +227,7 @@ let process_object oldenv dir sec_sp let r = { d_from = cb; d_modlist = work_alist; d_abstract = ids_to_discard } in - let op = Constant (spid,r,stre,cb.const_opaque,imp) in + let op = Constant (newsp,r,stre,cb.const_opaque,imp) in (op :: ops, ids_to_discard, (mods@constl, indl, cstrl)) | "INDUCTIVE" -> @@ -287,11 +288,9 @@ let process_operation = function | Parameter (spid,typ,imp) -> let _ = with_implicits imp (declare_parameter spid) typ in constant_message spid - | Constant (spid,r,stre,opa,imp) -> - let _ = - with_implicits imp (declare_constant spid) (ConstantRecipe r,stre,opa) - in - constant_message spid + | Constant (sp,r,stre,opa,imp) -> + with_implicits imp (redeclare_constant sp) (ConstantRecipe r,stre,opa); + constant_message (basename sp) | Inductive (mie,imp) -> let _ = with_implicits imp declare_mind mie in inductive_message mie.mind_entry_inds |