From f5e8da3bbf50e7a826398a05ba7c5cfafe667a6e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Mar 2004 11:00:04 +0000
Subject: Distinction entre declarations internes (p.ex. _subproof) et
 declarations utilisateurs pour export xml

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 695bb3bc7a..989944ae99 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1904,7 +1904,7 @@ let abstract_subproof name tac gls =
 	(delete_current_proof(); raise e)
     in   (* Faudrait un peu fonctionnaliser cela *)
     let cd = Entries.DefinitionEntry const in
-    let sp = Declare.declare_constant na (cd,IsProof Lemma) in
+    let sp = Declare.declare_internal_constant na (cd,IsProof Lemma) in
     let newenv = Global.env() in
     constr_of_reference (ConstRef (snd sp))
   in
-- 
cgit v1.2.3