From 752bbca071d0a9e5ddb1cd24db23a0df631cdc25 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 5 Jan 2004 21:48:14 +0000
Subject: Defaut d'information affichage en cas de notation incompatible

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5173 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 713127c767..5e32e55477 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -675,6 +675,7 @@ let pr_arg_level from = function
   | (n,L) when n=from -> str "at next level"
   | (n,E) -> str "at level " ++ int n
   | (n,L) -> str "at level below " ++ int n
+  | (n,Prec m) when m=n -> str "at level " ++ int n
   | (n,_) -> str "Unknown level"
 
 let pr_level ntn (from,args) =
-- 
cgit v1.2.3