diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d305a58ccc..9a9e0b9692 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -419,7 +419,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ~name:fname ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.Definition pl + ~kind:Decls.Definition pl bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left |