From e52a9fa8835eddf70d0c8e454470fb12eebef7cd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 30 Oct 2003 14:29:39 +0000
Subject: Parsing du moins unaire au niveau de l'application qui n'a pas besoin
 d'etre associative a gauche; gestion du signe dans le parseur pas dans
 l'interpreteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constrnew.ml4 | 5 +++--
 parsing/pcoq.ml4        | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index d5d1db939e..ea736cc91f 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -178,9 +178,10 @@ GEXTEND Gram
     | "90" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
       | c1 = operconstr; "->"; c2 = operconstr    -> CArrow(loc,c1,c2) ]
-    | "10" LEFTA
+    | "10"
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
-      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
+      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args)
+      | "-"; n=INT -> CNumeral (loc,Bignat.NEG (Bignat.of_string n)) ]
     | "9" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 152141bfae..5380115e1e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -547,7 +547,7 @@ let default_levels_v8 =
    100,Gramext.RightA;
    99,Gramext.RightA;
    90,Gramext.RightA;
-   10,Gramext.LeftA;
+   10,Gramext.RightA;
    9,Gramext.RightA;
    1,Gramext.LeftA;
    0,Gramext.RightA]
-- 
cgit v1.2.3