From d98dfbcae463f8d699765e2d7004becd7714d6cf Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 13 Apr 2011 14:26:59 +0000
Subject: Add [Polymorphic] flag for defs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/invfun.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 426b496dd1..ce484ca236 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -788,7 +788,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	     Ensures by: obvious
 	     i*)
 	   (mk_correct_id f_id)
-	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+	   (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
 	 Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i));
@@ -840,7 +840,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	     Ensures by: obvious
 	     i*)
 	   (mk_complete_id f_id)
-	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+	   (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
 	 Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i));
-- 
cgit v1.2.3