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

diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
new file mode 100644
index 000000000..39c089be9
--- /dev/null
+++ b/vernac/lemmas.mli
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*  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 Term
+open Decl_kinds
+open Pfedit
+
+type 'a declaration_hook
+val mk_hook :
+  (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
+
+val call_hook :
+  Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
+
+(** A hook start_proof calls on the type of the definition being started *)
+val set_start_hook : (types -> unit) -> unit
+
+val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+  ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
+  ?sign:Environ.named_context_val -> types ->
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+   unit declaration_hook -> unit
+
+val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+  ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+  ?sign:Environ.named_context_val -> types ->
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+  (Evd.evar_universe_context option -> unit declaration_hook) -> unit
+
+val start_proof_com :
+  ?inference_hook:Pretyping.inference_hook ->
+  goal_kind -> Vernacexpr.proof_expr list ->
+  unit declaration_hook -> unit
+
+val start_proof_with_initialization : 
+  goal_kind -> Evd.evar_map ->
+  (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
+  ((Id.t * universe_binders option) *
+     (types * (Name.t list * Impargs.manual_explicitation list))) list
+  -> int list option -> unit declaration_hook -> unit
+
+val universe_proof_terminator :
+  Proof_global.lemma_possible_guards ->
+    (Evd.evar_universe_context option -> unit declaration_hook) ->
+    Proof_global.proof_terminator
+
+val standard_proof_terminator :
+  Proof_global.lemma_possible_guards -> unit declaration_hook ->
+    Proof_global.proof_terminator
+
+(** {6 ... } *)
+
+(** A hook the next three functions pass to cook_proof *)
+val set_save_hook : (Proof.proof -> unit) -> unit
+
+val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
+
+
+(** [get_current_context ()] returns the evar context and env of the
+   current open proof if any, otherwise returns the empty evar context
+   and the current global env *)
+
+val get_current_context : unit -> Evd.evar_map * Environ.env