diff options
| author | filliatr | 1999-12-13 13:42:04 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-13 13:42:04 +0000 |
| commit | decb8c16274487ce3cac1e7d5de529b46b6d68e3 (patch) | |
| tree | 02a41980403e4c3fbeab8259a95ea14ba1b80e65 /proofs | |
| parent | 7dfacfe208a9fa5ad5f7669537c54609b4adf51e (diff) | |
- 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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |