From 35180e3a927d4450406ebeb0e89fdcde1341650a Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 28 Jan 2006 23:07:59 +0000
Subject: Réorganisation de la structure interne des types de déclarations
 (decl_kinds)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'contrib/funind/tacinv.ml4')

diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index bf918ba56..c2410d55c 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -842,7 +842,7 @@ let declareFunScheme f fname mutflist =
   const_entry_type = None;
   const_entry_opaque = false;
   const_entry_boxed = true } in
- let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition)) in
+ let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition Scheme)) in
  ()
 
 
-- 
cgit v1.2.3