From b789106117653fec8340ecbd88866c254fe1201d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 25 Sep 2017 18:01:38 +0200 Subject: Fixing a little parsing bug with level 90 introduced in 3e70ea9c. Unfortunately, some manual synchronization is needed between the constr parser and the table of constr/pattern levels. We do this synchronization which was missing in the commit moving "x -> y" to a user-level notation. --- parsing/egramcoq.ml | 2 ++ parsing/g_constr.ml4 | 1 + 2 files changed, 3 insertions(+) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 870137ca1..d51b8b54e 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -34,6 +34,7 @@ let default_levels = [200,Extend.RightA,false; 100,Extend.RightA,false; 99,Extend.RightA,true; + 90,Extend.RightA,true; 10,Extend.RightA,false; 9,Extend.RightA,false; 8,Extend.RightA,true; @@ -44,6 +45,7 @@ let default_pattern_levels = [200,Extend.RightA,true; 100,Extend.RightA,false; 99,Extend.RightA,true; + 90,Extend.RightA,true; 11,Extend.LeftA,false; 10,Extend.RightA,false; 1,Extend.LeftA,false; diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 7d0728458..ad8c1c398 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -376,6 +376,7 @@ GEXTEND Gram | "100" RIGHTA [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ] | "99" RIGHTA [ ] + | "90" RIGHTA [ ] | "11" LEFTA [ p = pattern; "as"; id = ident -> CAst.make ~loc:!@loc @@ CPatAlias (p, id) ] -- cgit v1.2.3