From aa49b010e2a7ff849c1569662d70bc251c056dfa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 13 Oct 2003 09:14:45 +0000
Subject: Petits bugs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4612 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 593d0f7a3b..b9150a30e3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -509,8 +509,8 @@ let vernac_require import _ qidl =
 	  warning ("Module "^(string_of_qualid qid)^
 	  " is now built-in and shouldn't be required")) qidl
     else
-      if not !Options.v7 then List.iter test_renamed_module qidl;
-      raise e
+      (if not !Options.v7 then List.iter test_renamed_module qidl;
+       raise e)
       
 let vernac_import export refl =
   let import_one ref = 
@@ -977,9 +977,9 @@ let vernac_show = function
 	| None -> pr_open_subgoals ()
 	| Some n -> pr_nth_open_subgoal n)
   | ShowGoalImplicitly None ->
-      msg (Constrextern.with_implicits pr_open_subgoals ())
+      Constrextern.with_implicits msg (pr_open_subgoals ())
   | ShowGoalImplicitly (Some n) ->
-      msg (Constrextern.with_implicits pr_nth_open_subgoal n)
+      Constrextern.with_implicits msg (pr_nth_open_subgoal n)
   | ShowProof -> show_proof ()
   | ShowNode -> show_node ()
   | ShowScript -> show_script ()
-- 
cgit v1.2.3