diff options
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 8aeff61e6..6dc36decf 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -904,7 +904,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive) } in *) let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) - Command.build_mutual [(indexpr,None)] true (* means: not coinductive *) + let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,None)] in + let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in + (* Declare the mutual inductive block with its associated schemes *) + ignore (Command.declare_mutual_inductive_with_eliminations false mie impls) (* Find infos on identifier id. *) |