diff options
| author | herbelin | 2001-11-19 10:38:25 +0000 |
|---|---|---|
| committer | herbelin | 2001-11-19 10:38:25 +0000 |
| commit | 79ac780518b797b9e2181ef3993cb08c202b130a (patch) | |
| tree | ab5ecd5546cc33b6aaa65afd4875c7560abfc64c /contrib/xml/xmlcommand.ml | |
| parent | 458fdba7a34fdf49f4f93e6734e90c6603c61adf (diff) | |
Mise en place d'une méthode directe pour indiquer le type des déclarations à toplevel plutôt que de passer par mkCast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -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 -> |