diff options
| author | msozeau | 2007-04-17 18:06:59 +0000 |
|---|---|---|
| committer | msozeau | 2007-04-17 18:06:59 +0000 |
| commit | 54edcf4a4dbddbdf2a17a3dab2b4c244a5cd7db0 (patch) | |
| tree | 9685ddc8760b91e38b3b6400bc1e48de84464d0b /toplevel/command.ml | |
| parent | e477e48354538a74339746df980b2514cdb5b010 (diff) | |
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
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 8 |
1 files 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 () |