diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-17 09:55:50 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-17 09:55:50 +0000 |
commit | f511a34d6de3b5be9b6a165dbd44b2dcfc8b6059 (patch) | |
tree | 22d8e2bce54c03da05e93ffcc853ae825d525adc /interp | |
parent | b264323d8f3fe7f0ef11d80eb90d3d0fb9c80832 (diff) |
Message d'erreur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6315 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r-- | interp/symbols.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/symbols.ml b/interp/symbols.ml index 5c9e00368..b54c3323b 100644 --- a/interp/symbols.ml +++ b/interp/symbols.ml @@ -270,7 +270,7 @@ let declare_notation_interpretation ntn scopt pat df pp8only = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in if Stringmap.mem ntn sc.notations && Options.is_verbose () then - warning ("Notation "^ntn^" is already used"^ + warning ("Notation "^ntn^" was already used"^ (if scopt = None then "" else " in scope "^scope)); let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in scope_map := Stringmap.add scope sc !scope_map; |