diff options
author | 2017-12-18 09:38:18 +0100 | |
---|---|---|
committer | 2017-12-18 09:38:18 +0100 | |
commit | 3da76841125ef48889c8eceb134116e2d0bd7a2e (patch) | |
tree | 8728b456dab71560379044459e7a7c979a1b252b /plugins/funind/merge.ml | |
parent | 0168ee0b6463a9ef44d768b0020b34785986c1cb (diff) | |
parent | 1172b52735a299dfc91aee36b30b576dfeff581c (diff) |
Merge PR #6419: [vernac] Split `command.ml` into separate files.
Diffstat (limited to 'plugins/funind/merge.ml')
-rw-r--r-- | plugins/funind/merge.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9e2774ff3..9fcb35f89 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -889,11 +889,11 @@ let merge_inductive (ind1: inductive) (ind2: inductive) } in *) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) - let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = Command.interp_mutual_inductive indl [] + let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in + let mie,pl,impls = ComInductive.interp_mutual_inductive indl [] false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) + ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) |