From d6e4513b844dbd551164868819c3a6ac9baf6c45 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 18 Mar 2014 16:20:57 +0100
Subject: STM: make -async-proofs on work from coqc too

---
 library/declaremods.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/declaremods.ml')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 2b917587c..bb623b7a1 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -874,8 +874,8 @@ let start_library dir =
   Lib.add_frozen_state ()
 
 let end_library dir =
-  let prefix, lib_stack = Lib.end_compilation dir in
   let mp,cenv,ast = Global.export dir in
+  let prefix, lib_stack = Lib.end_compilation dir in
   assert (ModPath.equal mp (MPfile dir));
   let substitute, keep, _ = Lib.classify_segment lib_stack in
   cenv,(substitute,keep),ast
-- 
cgit v1.2.3