diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 79348a7040..7b6303130b 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -861,8 +861,10 @@ let print_object lobj id sp dn fv env = let (_,(_,varentry,_)) = Declare.out_variable lobj in begin match varentry with - Declare.SectionLocalDef body -> - let typ = Retyping.get_type_of env Evd.empty body in + Declare.SectionLocalDef (body,optt) -> + let typ = match optt with + | None -> Retyping.get_type_of env Evd.empty body + | Some t -> t in add_to_pvars (Definition (N.string_of_id id, body, typ)) ; print_variable id (Some body) typ env inner_types | Declare.SectionLocalAssum typ -> |