From db6c97df4dde8b1ccb2e5b314a4747f66fd524c1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 13 Mar 2006 17:38:17 +0000
Subject: Update of Subtac contrib. Add {wf n R} as an alternative to {struct
 n}. May cause make world to fail because of dependency problems, make depend
 clean world should fix that (hopefully).

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

(limited to 'contrib/funind')

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 606352d220..c1c835b923 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -304,7 +304,7 @@ let do_generate_principle fixpoint_exprl  =
 			 snd
 			 (Topconstr.names_of_local_assums args) 
 		     in 
-		     let annot = Util.list_index (Name id) names - 1 in 
+		     let annot = Util.list_index (Name id) names - 1, Topconstr.CStructRec in 
  		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation) 
 		 | (name,None,args,types,body),recdef -> 
 		     let names =  (Topconstr.names_of_local_assums args) in
@@ -313,7 +313,7 @@ let do_generate_principle fixpoint_exprl  =
 			 (Util.dummy_loc,"GenFixpoint",
 			  Pp.str "the recursive argument needs to be specified")
 		     else 
-		       (name,0,args,types,body),(None:Vernacexpr.decl_notation)
+		       (name,(0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
 		     error 
 		       ("Cannot use mutual definition with well-founded recursion")
-- 
cgit v1.2.3