diff options
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") |