From a3a5350786ace6fac2c12890df6330782201cc77 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Aug 2002 09:24:32 +0000
Subject: Suppression automatique du corps des définitions locales opaques dans
 les contextes de preuves

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2972 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/xmlcommand.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index a2baceade2..14d0f94ac0 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -871,7 +871,7 @@ let print_object lobj id (sp,kn) dn fv env =
           let (_,(_,varentry,_)) = Declare.out_variable lobj in
            begin
             match varentry with
-               Declare.SectionLocalDef (body,optt) ->
+               Declare.SectionLocalDef (body,optt,_) ->
                  let typ = match optt with
 		   | None -> Retyping.get_type_of env Evd.empty body 
 		   | Some t -> t in
-- 
cgit v1.2.3