From fbad13370ba5a24423e9c0931a1e4524e53108f6 Mon Sep 17 00:00:00 2001
From: sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 5 Jul 2004 11:24:36 +0000
Subject: Constants just after a "Let id : t. ... Qed" local variable
 declaration were exported as a copy of the variable id. Fixed.

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

(limited to 'contrib/xml')

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 814266468..7b7ebd1dc 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -604,7 +604,8 @@ let _ =
   Declare.set_xml_declare_variable
    (function (sp,kn) ->
      let id = Libnames.basename sp in
-     print false (Libnames.VarRef id) (kind_of_variable id) xml_library_root)
+     print false (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
+     proof_to_export := None)
 ;;
 
 let _ =
-- 
cgit v1.2.3