[stm] Break stm/toplevel dependency loop.

Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.

This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.

As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.

Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.

1 files changed, 49 insertions, 0 deletions

diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
new file mode 100644
index 000000000..e5d79fd51
--- /dev/null
+++ b/vernac/indschemes.mli
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
+open Names
+open Term
+open Environ
+open Vernacexpr
+open Misctypes
+
+(** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
+
+(** Build and register the boolean equalities associated to an inductive type *)
+
+val declare_beq_scheme : mutual_inductive -> unit
+
+val declare_eq_decidability : mutual_inductive -> unit
+
+(** Build and register a congruence scheme for an equality-like inductive type *)
+
+val declare_congr_scheme : inductive -> unit
+
+(** Build and register rewriting schemes for an equality-like inductive type *)
+
+val declare_rewriting_schemes : inductive -> unit
+
+(** Mutual Minimality/Induction scheme *)
+
+val do_mutual_induction_scheme :
+  (Id.t located * bool * inductive * glob_sort) list -> unit
+
+(** Main calls to interpret the Scheme command *)
+
+val do_scheme : (Id.t located option * scheme) list -> unit
+
+(** Combine a list of schemes into a conjunction of them *)
+
+val build_combined_scheme : env -> constant list -> constr * types
+
+val do_combined_scheme : Id.t located -> Id.t located list -> unit
+
+(** Hook called at each inductive type definition *)
+
+val declare_default_schemes : mutual_inductive -> unit