[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, 66 insertions, 0 deletions

diff --git a/vernac/classes.mli b/vernac/classes.mli
new file mode 100644
index 000000000..d2cb788ea
--- /dev/null
+++ b/vernac/classes.mli
@@ -0,0 +1,66 @@
+(************************************************************************)
+(*  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 Names
+open Environ
+open Constrexpr
+open Typeclasses
+open Libnames
+
+(** Errors *)
+
+val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a
+
+val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
+
+(** Instance declaration *)
+
+val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit
+(** globality, reference, optional priority and pattern information *)
+
+val declare_instance_constant :
+  typeclass ->
+  Vernacexpr.hint_info_expr -> (** priority *)
+  bool -> (** globality *)
+  Impargs.manual_explicitation list -> (** implicits *)
+  ?hook:(Globnames.global_reference -> unit) ->
+  Id.t -> (** name *)
+  Id.t Loc.located list option ->
+  bool -> (* polymorphic *)
+  Evd.evar_map -> (* Universes *)
+  Constr.t -> (** body *)
+  Term.types -> (** type *)
+  Names.Id.t
+
+val new_instance :
+  ?abstract:bool -> (** Not abstract by default. *)
+  ?global:bool -> (** Not global by default. *)
+  ?refine:bool -> (** Allow refinement *)
+  Decl_kinds.polymorphic ->
+  local_binder list ->
+  typeclass_constraint ->
+  (bool * constr_expr) option ->
+  ?generalize:bool ->
+  ?tac:unit Proofview.tactic  ->
+  ?hook:(Globnames.global_reference -> unit) ->
+  Vernacexpr.hint_info_expr ->
+  Id.t
+
+(** Setting opacity *)
+
+val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
+
+(** For generation on names based on classes only *)
+
+val id_of_class : typeclass -> Id.t
+
+(** Context command *)
+
+(** returns [false] if, for lack of section, it declares an assumption
+    (unless in a module type). *)
+val context : Decl_kinds.polymorphic -> local_binder list -> bool