From 7c24910179fa07fe5ffdcce936ff3a057feacf8b Mon Sep 17 00:00:00 2001
From: bertot
Date: Fri, 17 Feb 2006 14:11:43 +0000
Subject: bug correction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8056 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/recdef/recdef.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index b07a587d14..79fe16f5a0 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1023,8 +1023,8 @@ let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_
 (*     let _ = message "start second proof" in *)
     com_eqn equation_id functional_ref f_ref term_ref eq;
     let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
-    generate_induction_principle
-      functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
+(*     generate_induction_principle *)
+(*       functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; *)
     ()
 
   in
-- 
cgit v1.2.3