From bad0063344bb14f1b457dbae7a9045d9e831f8ae Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 1 Dec 1999 10:54:05 +0000
Subject: portage Vernacentries (debut)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@173 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/mltop.ml         | 2 +-
 toplevel/vernacentries.ml | 7 ++++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 3928f63547..1f15fe0f1f 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -222,7 +222,7 @@ let (inMLModule,outMLModule) =
                     specification_function = specification_ml_module_object })
 
 let declare_ml_modules l =
-  Lib.add_anonymous_leaf (inMLModule {mnames=l})
+  let _ = Lib.add_anonymous_leaf (inMLModule {mnames=l}) in ()
     
 let print_ml_path () =
   let l = !coq_mlpath_copy in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 69d2dfbef0..7bf010646a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -4,12 +4,13 @@
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
 open Pp
+open Stamps
 open System
 open Names
 open Term
 open Reduction
-open Tacmach
 open Pfedit
+open Tacmach
 open Proof_trees
 open Library
 open Libobject
@@ -41,13 +42,13 @@ let show_script () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  mSGNL(Refiner.print_script true (ts_it evc) (initial_sign()) pf)
+  mSGNL(Refiner.print_script true (ts_it evc) (Global.var_context()) pf)
 
 let show_prooftree () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  mSG(Refiner.print_proof (ts_it evc) (initial_sign()) pf)
+  mSG(Refiner.print_proof (ts_it evc) (Global.var_context()) pf)
 
 let show_open_subgoals () =
   let pfts = get_pftreestate () in
-- 
cgit v1.2.3