From 54edcf4a4dbddbdf2a17a3dab2b4c244a5cd7db0 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 17 Apr 2007 18:06:59 +0000
Subject: Reorder hook and printing of message, more natural this way.

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

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 12146cdee4..f73fe5e9cf 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -764,8 +764,8 @@ let save id const (locality,kind) hook =
         let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn) in
   Pfedit.delete_current_proof ();
-  hook l r;
-  definition_message id
+  definition_message id;
+  hook l r
 
 let save_named opacity =
   let id,(const,persistence,hook) = Pfedit.cook_proof () in
@@ -801,8 +801,8 @@ let admit () =
   let kn =
     declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in
   Pfedit.delete_current_proof ();
-  hook Global (ConstRef kn);
-  assumption_message id
+  assumption_message id;
+  hook Global (ConstRef kn)
 
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
-- 
cgit v1.2.3