From fa9df2efe5666789bf91bb7761567cd53e6c451f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 18 Dec 2016 18:14:58 +0100
Subject: [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.
---
 proofs/proof_global.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index a2ee622215..120cde5e55 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -317,7 +317,10 @@ let constrain_variables init uctx =
   let cstrs = UState.constrain_variables levels uctx in
   Univ.ContextSet.add_constraints cstrs (UState.context_set uctx)
 
-let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+
+let close_proof ~keep_body_ucst_separate ?feedback_id ~now
+                (fpl : closed_proof_output Future.computation) =
   let { pid; section_vars; strength; proof; terminator; universe_binders } =
     cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
@@ -395,8 +398,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
     universes = (universes, binders) },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
-
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
-- 
cgit v1.2.3