From decb8c16274487ce3cac1e7d5de529b46b6d68e3 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 13 Dec 1999 13:42:04 +0000
Subject:  - méthode load sur les Hints  - CAST pris en compte dans Astterm  -
 Coercin.lookup_path_to_sort_from protégé par un try/with

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

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ab2a0c5135..4b3b797bf8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -178,7 +178,7 @@ let save_named opacity =
     ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
      strength);
   del_proof ident;
-  message(ident ^ " is defined")
+  if Options.is_verbose() then message (ident ^ " is defined")
     
 let save_anonymous opacity save_ident n =
   let (pfs,ts) = get_state() 
@@ -197,7 +197,7 @@ let save_anonymous opacity save_ident n =
        strength)
   end;
   del_proof ident;
-  message(save_ident ^ " is defined")
+  if Options.is_verbose() then message (save_ident ^ " is defined")
     
 let save_anonymous_thm opacity id =
   save_anonymous opacity id NeverDischarge
-- 
cgit v1.2.3