diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/library/declare.ml b/library/declare.ml index da2c1b778..278acc665 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -57,7 +57,7 @@ let set_xml_declare_inductive f = xml_declare_inductive := if_xml f type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types + | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *) type variable_declaration = dir_path * section_variable_entry * logical_kind @@ -84,17 +84,17 @@ let cache_variable ((sp,_),o) = (* Constr raisonne sur les noms courts *) if Idmap.mem id !vartab then errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); - let vd = match d with (* Fails if not well-typed *) - | SectionLocalAssum ty -> + let vd,impl,keep = match d with (* Fails if not well-typed *) + | SectionLocalAssum (ty, impl, keep) -> let cst = Global.push_named_assum (id,ty) in let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalAssum (ty,cst) + CheckedSectionLocalAssum (ty,cst), impl, if keep then Some ty else None | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalDef (Option.get bd,ty,cst,opaq) in + CheckedSectionLocalDef (Option.get bd,ty,cst,opaq), false, None in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id; + add_section_variable id impl keep; Dischargedhypsmap.set_discharged_hyps sp []; vartab := Idmap.add id (p,vd,mk) !vartab |