From 7a5688f6e2421a706c16e23e445d42f39a82e74b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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/comDefinition.mli | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 vernac/comDefinition.mli

(limited to 'vernac/comDefinition.mli')

diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
new file mode 100644
index 000000000..8dcd31f25
--- /dev/null
+++ b/vernac/comDefinition.mli
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Entries
+open Decl_kinds
+open Redexpr
+open Constrexpr
+
+(** {6 Definitions/Let} *)
+
+val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
+  local_binder_expr list -> red_expr option -> constr_expr ->
+  constr_expr option -> unit Lemmas.declaration_hook -> unit
+
+(************************************************************************)
+(** Internal API  *)
+(************************************************************************)
+
+(** Not used anywhere. *)
+val interp_definition :
+  Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
+  constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
+                        Univdecls.universe_decl * Impargs.manual_implicits
-- 
cgit v1.2.3