diff options
| author | msozeau | 2006-03-13 17:38:17 +0000 |
|---|---|---|
| committer | msozeau | 2006-03-13 17:38:17 +0000 |
| commit | db6c97df4dde8b1ccb2e5b314a4747f66fd524c1 (patch) | |
| tree | 39ba546322e7f3d4bd4cc9d58260d3f1b4114bd5 /contrib/funind | |
| parent | d9cc734c4cd2a75a303cc08c3df0973077099ab1 (diff) | |
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
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/indfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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") |