aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/pcoq.ml45
1 files changed, 4 insertions, 1 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 5c6216687a..40e456061f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -484,7 +484,10 @@ let default_levels =
0,Gramext.RightA]
let default_pattern_levels =
- [10,Gramext.LeftA;
+ [200,Gramext.RightA;
+ 100,Gramext.LeftA;
+ 99,Gramext.RightA;
+ 10,Gramext.LeftA;
0,Gramext.RightA]
let level_stack =