From b04df941937814d3701c9d0f573d962d85f088cc Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 18 Nov 2003 18:54:38 +0000
Subject: reparation bug moins unaire (erreur de PP)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4944 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 26df4b837c..338f4092a2 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -779,14 +779,15 @@ let make_current_scopes (scopt,scopes) =
 let make_notation loc ntn l =
   match ntn,l with
     (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
-    | "- _", [CNumeral(_,Bignat.POS p)] -> CNotation (loc,"- ( _ )",l)
+    | "- _", [CNumeral(_,Bignat.POS p)] ->
+        CNotation (loc,ntn,[CNotation(loc,"( _ )",l)])
     | _ -> CNotation (loc,ntn,l)
 
 let make_pat_notation loc ntn l =
   match ntn,l with
     (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
     | "- _", [CPatNumeral(_,Bignat.POS p)] ->
-        CPatNotation (loc,"- ( _ )",l)
+        CPatNotation (loc,ntn,[CPatNotation(loc,"( _ )",l)])
     | _ -> CPatNotation (loc,ntn,l)
 
 
-- 
cgit v1.2.3