From 7a5688f6e2421a706c16e23e445d42f39a82e74b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 13 Dec 2017 07:18:22 +0100 Subject: [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. --- vernac/classes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index efaf6c0c0..3d9c7defa 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -411,7 +411,7 @@ let context poly l = in let nstatus = match b with | None -> - pi3 (Command.declare_assumption false decl (t, univs) Universes.empty_binders [] impl + pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> let decl = (Discharge, poly, Definition) in -- cgit v1.2.3