From 06f1e9bcd8f846628665a3d83b0e2b30e190f41e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Mar 2004 12:20:50 +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@5615 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/record.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 89cb35b74b..36d83bb28d 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -183,7 +183,7 @@ let declare_projections indsp coers fields =
                     const_entry_type = Some projtyp;
                     const_entry_opaque = false } in
 		  let k = (DefinitionEntry cie,IsDefinition) in
-		  let sp = declare_constant fid k in
+		  let sp = declare_internal_constant fid k in
 		  Options.if_verbose message (string_of_id fid ^" is defined");
 		  sp
                 with Type_errors.TypeError (ctx,te) ->
-- 
cgit v1.2.3