diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index 6e9835487..65d08dd81 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -92,7 +92,7 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in + CheckedSectionLocalDef (Option.get bd,ty,cst,opaq) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id; Dischargedhypsmap.set_discharged_hyps sp []; @@ -200,7 +200,7 @@ let hcons_constant_declaration = function let (hcons1_constr,_) = hcons_constr (hcons_names()) in DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; - const_entry_type = option_map hcons1_constr ce.const_entry_type; + const_entry_type = Option.map hcons1_constr ce.const_entry_type; const_entry_opaque = ce.const_entry_opaque; const_entry_boxed = ce.const_entry_boxed } | cd -> cd |