diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 07:18:22 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-17 10:56:04 +0100 |
commit | 7a5688f6e2421a706c16e23e445d42f39a82e74b (patch) | |
tree | 4dfc0054afb151a93e185ab21a51748e4b2086ea /plugins/funind/glob_term_to_relation.ml | |
parent | 53f5cc210da4debd5264d6d8651a76281b0b4256 (diff) |
[vernac] Split `command.ml` into separate files.
Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.
We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.
This patch depends on #6413.
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fa4353630..889c064b2 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1497,7 +1497,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) Decl_kinds.Finite with | UserError(s,msg) as e -> |