diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 0a7614b..b302ac7 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -14,7 +14,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.20'
+          - 'rocq/rocq-prover:9.0'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4
diff --git a/.gitignore b/.gitignore
index 1f0ab2c..3ffc21f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -20,3 +20,4 @@ ocamlgraph-1.7
 .merlin
 make_merlin.sh
 ott.install
+regression/regression
diff --git a/coq-ott.opam b/coq-ott.opam
index 7ef3dbb..d6f6920 100644
--- a/coq-ott.opam
+++ b/coq-ott.opam
@@ -18,7 +18,7 @@ this library.
 build: [make "-j%{jobs}%" "-C" "coq"]
 install: [make "-C" "coq" "install"]
 depends: [
-  "coq" {>= "8.14"}
+  ("coq" {>= "8.14" & < "9.0"}) | ("rocq-prover" {>= "9.0"} & "coq" {>= "9.0"})
 ]
 tags: [
   "category:Computer Science/Semantics and Compilation/Semantics"
diff --git a/regression/Makefile b/regression/Makefile
index da75cef..202cb98 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -36,11 +36,11 @@
 all: regression
 
 regression: regression.ml
-	ocamlc unix.cma str.cma -o regression -dtypes regression.ml
+	ocamlc -I +unix -I +str unix.cma str.cma -o regression -dtypes regression.ml
 
 regression_p: regression_p_client.ml regression_p_master.ml
-	ocamlc unix.cma str.cma -o regression_p_client regression_p_client.ml
-	ocamlc unix.cma str.cma -o regression_p_master regression_p_master.ml
+	ocamlc -I +unix -I +str unix.cma str.cma -o regression_p_client regression_p_client.ml
+	ocamlc -I +unix -I +str unix.cma str.cma -o regression_p_master regression_p_master.ml
 
 regression_para: regression_para.ml
 	ocamlp3lopt -par unix.cmxa str.cmxa -o regression_para regression_para.ml
@@ -77,7 +77,7 @@ clean-regr:
 
 # Jenkins
 
-# regression-jenkins: 
+# regression-jenkins:
 # 	ocamlc unix.cma str.cma -o regression-jenkins -dtypes regression-jenkins.ml
 
 run-jenkins: regression
diff --git a/regression/baseline-2025-03.bl b/regression/baseline-2025-03.bl
new file mode 100644
index 0000000..55f7574
Binary files /dev/null and b/regression/baseline-2025-03.bl differ
diff --git a/regression/baseline-2025-03.txt b/regression/baseline-2025-03.txt
new file mode 100644
index 0000000..54ea8ae
--- /dev/null
+++ b/regression/baseline-2025-03.txt
@@ -0,0 +1,103 @@
+ Coq CoqNL Isa  HOL OCaml LaTeX
+ -    -    -    + +  -    + + ../tests/leroy-jfp96.ott
+ -    -    -    -    -    + + ../tests/test-j.ott
+ + -  + -  + -  + -  + -  + + ../tests/test-lj-list_ambiguity.ott
+ + +  + +  -    -    -    + - ../tests/test-mjp-trans.ott
+ + -  + -  + -  + -  + -  + + ../tests/test-mjp.ott
+ + +  + +  + +  + +  + +  + + ../tests/test-pottier1.ott
+ + +  + +  + +  + +  + -  + + ../tests/test1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test10.ott
+ + +  + +  + +  + +  -    + + ../tests/test10_homs.ott
+ + +  + +  + +  -    -    + + ../tests/test10_isasyn.ott
+ + +  + +  + +  + +  -    + + ../tests/test10st.ott
+ + -  + -  + -  -    -    + + ../tests/test10st_fe.ott
+ + +  + +  + +  + +  -    + + ../tests/test10st_first_half.ott
+ + +  + +  + +  + +  + +  + + ../tests/test11.ott
+ + +  + +  + +  + +  + +  + + ../tests/test12.ott
+ + +  + +  + +  + +  + +  + + ../tests/test13.ott
+ + -  + -  + -  + -  + +  + + ../tests/test13b.ott
+ + +  + +  + +  + +  + +  + + ../tests/test14.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.0.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.2.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.3.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.4.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.4b.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.4c.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.4d.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.5.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.6.ott
+ + +  + +  + +  + +  + +  + + ../tests/test15.7.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.0.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.2.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.3.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.4.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.5.ott
+ + +  + +  + +  + +  + +  + + ../tests/test16.6.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.0.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.1.ott
+ + +  + +  + -  + +  -    + + ../tests/test17.10.ott
+ + -  + -  + -  + +  -    + + ../tests/test17.11.ott
+ + +  + +  + -  + +  -    + + ../tests/test17.12.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.13.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.14.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.2.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.3.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.4.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.5.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.6.ott
+ + +  + +  + +  + +  + +  + + ../tests/test17.7.ott
+ + +  + +  + -  + +  + +  + + ../tests/test17.8.ott
+ + +  + +  + -  + +  + +  + + ../tests/test17.9.ott
+ + +  + +  + +  + +  + +  + + ../tests/test18.0.ott
+ + +  + +  + +  + +  + +  + + ../tests/test18.1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test18.2.ott
+ + -  + -  + -  + +  -    + + ../tests/test19.0.ott
+ + +  + +  + +  + -  + +  + + ../tests/test2.ott
+ -    -    -    -    -    + + ../tests/test3.ott
+ + +  + +  + +  + -  + -  + + ../tests/test4.ott
+ -    -    -    -    -    + + ../tests/test5.ott
+ -    -    -    -    -    + + ../tests/test6-tex.ott
+ -    -    -    -    -    + + ../tests/test6.ott
+ + -  + -  + +  + +  + +  + + ../tests/test8.ott
+ -    -    -    -    -    + + ../tests/test8p.ott
+ -    -    -    -    -    + + ../tests/test_jan_2006-09-08.ott
+ + -  + -  + -  + -  -    + + ../tests/test_lists_1.ott
+ + +  + +  + +  + -  + +  + + ../tests/test_lists_freevars_1.ott
+ + +  + +  + +  + +  -    + + sys-bool
+ + +  + +  + +  + +  -    + + sys-arith
+ + +  + +  + +  + +  -    + + sys-untyped
+ + +  + +  + -  + -  -    + + sys-puresimple
+ + +  + +  + +  + +  -    + + sys-tybool
+ + +  + +  + -  + +  -    + - sys-sortoffullsimple
+ + -  + -  + -  + -  -    + + sys-tuple
+ + +  + +  + +  + +  -    + + sys-puresub
+ + +  + +  + -  + +  -    + - sys-roughlyfullsimple
+ + -  + -  + -  + +  -    + + sys-purercdsub
+ -    -    -    -    -    -   ../tests/test_bind_aux_empty_1.ott
+ -    -    -    -    -    -   ../tests/test_bind_dots_1.ott
+ + +  + +  + -  + -  + -  + + ../tests/test_bind_isa_1.ott
+ + +  + +  + +  + -  + +  + + ../tests/test_coq_equality_x_1.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_defn_repeated_nonterminal_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_embed_top_1.ott
+ + -  + -  + -  + -  + +  + + ../tests/test_empty_defn.ott
+ + -  + -  + -  + -  -    + + ../tests/test_lists_1.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_lists_coq_bind_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_lists_coq_defn_subrule_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_lists_coq_defn_subrule_2.ott
+ + +  + +  + -  + +  + +  + + ../tests/test_lists_coq_defn_subrule_3.ott
+ + +  + +  + -  + -  + -  + + ../tests/test_lists_coq_defn_subrule_4.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_lists_coq_defn_tuple_1.ott
+ + +  + +  + -  + +  + +  + + ../tests/test_lists_coq_defn_tuple_2.ott
+ + +  + +  + -  + -  -    + - ../tests/test_lists_coq_list_functions_1.ott
+ + +  + +  + -  + +  + +  + + ../tests/test_lists_coq_list_functions_2.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_lists_defn_list_form_1.ott
+ + -  + -  + -  + +  -    + + ../tests/test_lists_coq_list_functions_3.ott
+ + -  + -  + -  + +  + +  + + ../tests/test_lists_coq_list_functions_4.ott
+ + +  + +  + -  + -  + +  + + ../tests/test_subrules_1.ott
+ -    -    -    -    -    -   ../tests/test_lists_terminal_1.ott
+ + +  + +  + -  + +  -    + + ../tests/test_embed_location_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_embed_top_1.ott
+ + +  + +  + +  + +  + +  + + ../tests/test_merge_embed_location_1-1.ott
+ + +  + +  + -  + +  -    + + ../tests/test_merge_embed_location_1-2.ott
diff --git a/regression/baseline-jenkins.txt b/regression/baseline-jenkins.txt
new file mode 100644
index 0000000..d294265
--- /dev/null
+++ b/regression/baseline-jenkins.txt
@@ -0,0 +1,102 @@
+ Coq CoqNL Isa  HOL OCaml LaTeX
+ -    -    -    + -  -    + + ../tests/leroy-jfp96.ott
+ -    -    -    -    -    + + ../tests/test-j.ott
+ + -  + -  + -  + -  + -  + + ../tests/test-lj-list_ambiguity.ott
+ + +  + -  -    -    -    + - ../tests/test-mjp-trans.ott
+ + -  + -  + -  + -  + -  + + ../tests/test-mjp.ott
+ + +  + -  + -  + +  + +  + + ../tests/test-pottier1.ott
+ + +  + -  + -  + +  + -  + + ../tests/test1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test10.ott
+ + +  + -  + -  + +  -    + + ../tests/test10_homs.ott
+ + +  + -  + -  -    -    + + ../tests/test10_isasyn.ott
+ + +  + -  + -  + +  -    + + ../tests/test10st.ott
+ + -  + -  + -  -    -    + + ../tests/test10st_fe.ott
+ + +  + -  + -  + +  -    + + ../tests/test10st_first_half.ott
+ + +  + -  + -  + +  + +  + + ../tests/test11.ott
+ + +  + -  + -  + +  + +  + + ../tests/test12.ott
+ + +  + -  + -  + +  + +  + + ../tests/test13.ott
+ + -  + -  + -  + -  + +  + + ../tests/test13b.ott
+ + +  + -  + -  + +  + +  + + ../tests/test14.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.0.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.2.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.3.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.4.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.4b.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.4c.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.4d.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.5.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.6.ott
+ + +  + -  + -  + +  + +  + + ../tests/test15.7.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.0.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.2.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.3.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.4.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.5.ott
+ + +  + -  + -  + +  + +  + + ../tests/test16.6.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.0.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.1.ott
+ + +  + -  + -  + +  -    + + ../tests/test17.10.ott
+ + +  + -  + -  + +  -    + + ../tests/test17.11.ott
+ + +  + -  + -  + +  -    + + ../tests/test17.12.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.13.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.14.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.2.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.3.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.4.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.5.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.6.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.7.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.8.ott
+ + +  + -  + -  + +  + +  + + ../tests/test17.9.ott
+ + +  + -  + -  + +  + +  + + ../tests/test18.0.ott
+ + +  + -  + -  + +  + +  + + ../tests/test18.1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test18.2.ott
+ + +  + -  + -  + +  -    + + ../tests/test19.0.ott
+ + +  + -  + -  + -  + +  + + ../tests/test2.ott
+ -    -    -    -    -    + + ../tests/test3.ott
+ + +  + -  + -  + -  + -  + + ../tests/test4.ott
+ -    -    -    -    -    + + ../tests/test5.ott
+ -    -    -    -    -    + + ../tests/test6-tex.ott
+ -    -    -    -    -    + + ../tests/test6.ott
+ + -  + -  + -  + +  + +  + + ../tests/test8.ott
+ -    -    -    -    -    + + ../tests/test8p.ott
+ -    -    -    -    -    + + ../tests/test_jan_2006-09-08.ott
+ + -  + -  + -  + -  -    + + ../tests/test_lists_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_lists_freevars_1.ott
+ + -  + -  + -  + +  -    + + sys-bool
+ + -  + -  + -  + +  -    + + sys-arith
+ + -  + -  + -  + +  -    + + sys-untyped
+ + -  + -  + -  + -  -    + + sys-puresimple
+ + -  + -  + -  + +  -    + + sys-tybool
+ + -  + -  + -  + +  -    + - sys-sortoffullsimple
+ + -  + -  + -  + -  -    + + sys-tuple
+ + -  + -  + -  + +  -    + + sys-puresub
+ + -  + -  + -  + +  -    + - sys-roughlyfullsimple
+ + -  + -  + -  + +  -    + + sys-purercdsub
+ -    -    -    -    -    -   ../tests/test_bind_aux_empty_1.ott
+ -    -    -    -    -    -   ../tests/test_bind_dots_1.ott
+ + +  + -  + -  + -  + -  + + ../tests/test_bind_isa_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_coq_equality_x_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_defn_repeated_nonterminal_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_embed_top_1.ott
+ + -  + -  + -  + -  + +  + + ../tests/test_empty_defn.ott
+ + -  + -  + -  + -  -    + + ../tests/test_lists_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_lists_coq_bind_1.ott
+ + -  + -  + -  + +  + +  + + ../tests/test_lists_coq_defn_subrule_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_lists_coq_defn_subrule_2.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_lists_coq_defn_subrule_3.ott
+ + -  + -  + -  + -  + +  + + ../tests/test_lists_coq_defn_tuple_1.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_lists_coq_defn_tuple_2.ott
+ + -  + -  + -  + -  -    + - ../tests/test_lists_coq_list_functions_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_lists_coq_list_functions_2.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_lists_defn_list_form_1.ott
+ + -  + -  + -  + +  -    + + ../tests/test_lists_coq_list_functions_3.ott
+ + -  + -  + -  + +  + +  + + ../tests/test_lists_coq_list_functions_4.ott
+ + +  + -  + -  + -  + +  + + ../tests/test_subrules_1.ott
+ -    -    -    -    -    -   ../tests/test_lists_terminal_1.ott
+ + +  + -  + -  + +  -    + + ../tests/test_embed_location_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_embed_top_1.ott
+ + +  + -  + -  + +  + +  + + ../tests/test_merge_embed_location_1-1.ott
+ + +  + -  + -  + +  -    + + ../tests/test_merge_embed_location_1-2.ott
diff --git a/regression/regression.ml b/regression/regression.ml
index 3cd122c..c50bec9 100644
--- a/regression/regression.ml
+++ b/regression/regression.ml
@@ -92,7 +92,7 @@ let latex_regressions = ref 0
 (* let twelf_progressions = ref 0 *)
 (* let twelf_regressions = ref 0 *)
 let summary = ref []
-let report_fd = ref Pervasives.stdout
+let report_fd = ref Stdlib.stdout
 let config_state = ref []
 
 let _ =
@@ -354,7 +354,7 @@ let run_test i n (tn,tl) =
     if (command cmd) = 0
     then begin
       pp_success tgt name;
-      let cmd = "coqc -init-file _ott_coqrc.v "^name^".v > " ^ name ^ ".coq.out" (* was "/dev/null"*)  in
+      let cmd = "coqc -Q ../coq Ott "^name^".v > " ^ name ^ ".coq.out" (* was "/dev/null"*)  in
       let tgt = "Coq" in
       pp_tgt i_of_n tgt cmd;
       if (command cmd) = 0 then begin
@@ -382,7 +382,7 @@ let run_test i n (tn,tl) =
     if (command cmd) = 0
     then begin
       pp_success tgt name;
-      let cmd = "coqc -init-file _ott_coqrc.v "^name^".v" in
+      let cmd = "coqc -Q ../coq Ott "^name^".v" in
       let tgt = "Coq" in
       pp_tgt i_of_n tgt cmd;
       if (command cmd) = 0 then begin
@@ -575,7 +575,7 @@ let report tp a b =
     progressions := !progressions + 1;
     ott_progressions := !ott_progressions + 1
   end else 
-    if not a.ott && b.ott 
+    if not a.ott && b.ott && not (a.tp = Skipped || b.tp = Skipped)
     then begin
       regressions := !regressions + 1;
       ott_regressions := !ott_regressions + 1
@@ -839,4 +839,6 @@ let _ =
     end;
     output_string fd "</testsuite>\n";
     close_out fd
-  end
+  end;
+
+  if !regressions != 0 then exit 1
diff --git a/regression/regression.otl b/regression/regression.otl
index 04d939d..dbc546b 100644
--- a/regression/regression.otl
+++ b/regression/regression.otl
@@ -86,6 +86,7 @@ sys-purercdsub : ../examples/tapl/common.ott ../examples/tapl/common_typing.ott
 ../tests/test_lists_coq_defn_subrule_1.ott
 ../tests/test_lists_coq_defn_subrule_2.ott
 ../tests/test_lists_coq_defn_subrule_3.ott
+../tests/test_lists_coq_defn_subrule_4.ott
 ../tests/test_lists_coq_defn_tuple_1.ott
 ../tests/test_lists_coq_defn_tuple_2.ott
 ../tests/test_lists_coq_list_functions_1.ott
diff --git a/regression/regression_p_client.ml b/regression/regression_p_client.ml
index 4246cbf..83f5ed8 100644
--- a/regression/regression_p_client.ml
+++ b/regression/regression_p_client.ml
@@ -71,7 +71,7 @@ let latex_regressions = ref 0
 let twelf_progressions = ref 0
 let twelf_regressions = ref 0
 let summary = ref []
-let report_fd = ref Pervasives.stdout
+let report_fd = ref Stdlib.stdout
 
 (* let _ = *)
 (*   putenv "CVSROOT" ":pserver:zappa@localhost:/usr/groups/netsem/dynsem/cvs"; *)
diff --git a/regression/regression_p_master.ml b/regression/regression_p_master.ml
index 5d21ab1..96d5160 100644
--- a/regression/regression_p_master.ml
+++ b/regression/regression_p_master.ml
@@ -67,7 +67,7 @@ let latex_progressions = ref 0
 let latex_regressions = ref 0
 let twelf_progressions = ref 0
 let twelf_regressions = ref 0
-let report_fd = ref Pervasives.stdout
+let report_fd = ref Stdlib.stdout
 
 (* let _ = *)
 (*   if !night then begin *)
diff --git a/regression/regression_para.ml b/regression/regression_para.ml
index 7645a8f..3798a74 100644
--- a/regression/regression_para.ml
+++ b/regression/regression_para.ml
@@ -83,7 +83,7 @@ let latex_regressions = ref 0
 let twelf_progressions = ref 0
 let twelf_regressions = ref 0
 let summary = ref []
-let report_fd = ref Pervasives.stdout
+let report_fd = ref Stdlib.stdout
 let config_state = ref []
 
 let _ =
diff --git a/revision_history.txt b/revision_history.txt
index 9223f06..1c7cefe 100644
--- a/revision_history.txt
+++ b/revision_history.txt
@@ -2,13 +2,13 @@
 2006.11.01  Version 0.04.2
 2006.12.20  Version 0.10     initial public release
 
-2006.12.20  Version 0.10.1  
+2006.12.20  Version 0.10.1
 - include missing HOL file ottDefine.sml
 
-2006.12.22  Version 0.10.2  
+2006.12.22  Version 0.10.2
 - include missing ottmode.el
 
-2007.01.19  Version 0.10.3   
+2007.01.19  Version 0.10.3
 - bugfixes
 - new examples: various TAPL fragments, and an OCaml fragment with
    concurrency (peterson_caml.ott)
@@ -19,7 +19,7 @@
 
 2007.01.24  Version 0.10.4
 - bugfix: allow "-" in bindspec lexing
-  
+
 2007.02.07  Version 0.10.5
 - various bugfixes (mostly w.r.t. Coq list support)
 - various improvements to examples
@@ -51,14 +51,14 @@
 - add missing file from Coq proof support: ott_list_eq_dec.v
 
 2007.10.18  Version 0.10.13
-- new (experimental!) switch -picky_multiple_parses <true>,     
+- new (experimental!) switch -picky_multiple_parses <true>,
    to allow multiple parses if the generated code is
    identical - at present only for filtered LaTeX
 - some source documentation
- 
+
 2008.02.15  Version 0.10.14
 - new parser, with better performance and better support for disambiguation
-   (see Section 14 "Parsing Priorities" in the manual, and changes to 
+   (see Section 14 "Parsing Priorities" in the manual, and changes to
    Section 20 "Reference: The language of symbolic terms")
 - new support for context grammars, with automatically generated
    hole-filling functions (see Section 13 "Context rules" in the manual)
@@ -83,7 +83,7 @@
 
 - fix ocamlvar hom bug
 - fix bug in Coq backend when dealing with some kinds of dot forms
-- suppress printing of number of good/bad definition rules if 
+- suppress printing of number of good/bad definition rules if
    there are no rules
 - change -tex_show_meta false behaviour to not suppress sugar
    productions
@@ -92,13 +92,12 @@
    be easy to build from source, but we don't have access to a
    suitable machine.
 
-
 2010.3.24 Version 0.10.18alpha
 
 - The previous command-line options -coq, -hol, etc., are no longer
-  supported; they should be replaced by -o. 
+  supported; they should be replaced by -o.
 
-- By default (unless -merge true is set) the order of the input file 
+- By default (unless -merge true is set) the order of the input file
   is preserved, so one can have mixed sequences of definitions of
   grammar, of inductive relations, and of embed blocks.
 
@@ -113,7 +112,7 @@
 
 - Better tex default spacing, distinguishing alphabetic and other
   ("symbolic") terminals based on their ott source strings and
-  wrapping them in \ottkw{} and \ottsym{} respectively. 
+  wrapping them in \ottkw{} and \ottsym{} respectively.
 
 - Support for in-line prover code in premises, e.g.
 
@@ -124,7 +123,7 @@
 - The {{ phantom }} hom can now be applied to metavariables and to
   nonterminal rules.  In both cases it suppresses generation of a prover
   or OCaml definition, but any type homs are taken into account when
-  the metavariable or nonterminal root is output as a type. 
+  the metavariable or nonterminal root is output as a type.
 
 - There is a new hom {{ order ... }} that can be applied to
   productions which lets one specify the order of arguments of a
@@ -135,11 +134,11 @@
 
 - There is a new hom {{ coq-universe UniverseName }} that can be
   applied to metavariable or nonterminal rules, eg to force Ott to
-  generate definitions in Type instead of in Set. 
+  generate definitions in Type instead of in Set.
 
 - Changed some debug options (eg show-pre-sort)
 
-- Ocaml list homs on productions are now permitted 
+- Ocaml list homs on productions are now permitted
 
 - add coq_lngen option for compatibility with the lngen tool
 
@@ -153,11 +152,10 @@
    - performance issue when using contextrules [Nicolas Pouillard]
    - parens in OCaml substitutions for multiple binders [Vilhelm Sjoberg]
 
-
 2010.03.29 Version 0.20
 
 - The order among mutually recursive nonterminal definitions in
-  grammar blocks is now preserved in prover output. 
+  grammar blocks is now preserved in prover output.
 
 2010.04.04 Version 0.20.1
 
@@ -169,11 +167,9 @@
      defn
      t1 --> t2 :: ::reduce::'' by
 
-
         --------------------------  :: ax_app
         (\x.t1) v2 -->  {v2/x}t1
 
-
 2010.06.29
 
 - refactor the generated latex for grammars so that condensed grammars
@@ -184,7 +180,7 @@
     \renewcommand{\ottprodline}[6]{{}\ ${}#1$\mbox{\ {}$#2$}{}}
     \renewcommand{\ottfirstprodline}[6]{{}\ ${}$\mbox{\ {}$#2$}{}}
     \renewcommand{\ottprodnewline}{}
-    \renewcommand{\ottinterrule}{\\[1mm]} 
+    \renewcommand{\ottinterrule}{\\[1mm]}
 
 - add experimental option (-ocaml_include_terminals true) to include, in
    generated OCaml types, an instance of "terminal" in all the places
@@ -194,7 +190,7 @@
 
 2010.11.28 Version 0.20.3
 
-- fixes to bugs: 
+- fixes to bugs:
 
     11367 coq-universe Type problem with non-native lists
     11368 generation of induction principles in Ott 0.20
@@ -206,7 +202,7 @@
    inductive rules for the Coq backend.  For instance, adding the
    [[:RED]] annotation below
 
-   t1 --> t1' [[:RED]] 
+   t1 --> t1' [[:RED]]
    -------------------- :: ctx_app_arg
    v t1 --> v t1'
 
@@ -226,24 +222,24 @@
    names the user specified in the definition of grammar rules.  For
    instance the grammar definition below
 
-     grammar 
-     term, t :: 't_' ::=                               
-       | x            ::  :: Var                  
+     grammar
+     term, t :: 't_' ::=
+       | x            ::  :: Var
        | \ x . t      ::  :: Lam     (+ bind x in t +)
-       | t t'         ::  :: App                  
-       | ( t )        :: S:: Paren   {{ icho [[t]]  }} 
+       | t t'         ::  :: App
+       | ( t )        :: S:: Paren   {{ icho [[t]]  }}
        | { t / x } t' :: M:: Tsub    {{ icho (tsubst_t [[t]] [[x]] [[t']])}}
 
    generates
 
-     Inductive term : Set := 
+     Inductive term : Set :=
       | t_var (x:var)
       | t_lam (x:var) (t:term)
       | t_app (t:term) (t':term).
 
-   instead of 
+   instead of
 
-     Inductive term : Set := 
+     Inductive term : Set :=
       | t_var : var -> term
       | t_lam : var -> term -> term
       | t_app : term -> term -> term.
@@ -262,14 +258,14 @@
   in the Ott file below:
 
     grammar
-     n :: 'n_' ::= 
+     n :: 'n_' ::=
        | 0       :: :: Zero
        | S n     :: :: Succ
 
     funs
       Add ::=  {{ hol-proof ... }}
     fun
-      n1 + n2 :: n :: add {{ com a function of type num \to num \to num }} 
+      n1 + n2 :: n :: add {{ com a function of type num \to num \to num }}
     by
       0 + n2 === n2
       S n1 + n2 === n1 + S n2
@@ -279,7 +275,7 @@
     Fixpoint add (x1:num) (x2:num) : num:=
       match x1,x2 with
       | n_zero , n2 => n2
-      | (n_succ n1) , n2 =>  (add n1 (n_succ n2) ) 
+      | (n_succ n1) , n2 =>  (add n1 (n_succ n2) )
     end.
 
   The "fun n1 + n2 :: n :: add by" declaration specifies:
@@ -307,7 +303,7 @@
   Coq).  Added the -coq_use_filter_fn option for backwards
   compatibility (*).
 
-- Introduced a new embed hom 
+- Introduced a new embed hom
 
       embed {{ coq-lib foo1 foo2 foo3 }}
 
@@ -337,13 +333,13 @@ This version fixes a packaging problem of the version 0.21.
   inside.  The existing syntax {{ ... }} is also valid.
 
 - Added embed tex-wrap-pre/tex-wrap-post homs to customize tex
-  wrapping: the default LaTeX header can be changed by writing 
+  wrapping: the default LaTeX header can be changed by writing
 
-    embed {{ tex-wrap-pre ... }} 
+    embed {{ tex-wrap-pre ... }}
 
-  and the default footer by writing 
+  and the default footer by writing
 
-    embed {{ tex-wrap-post ... }}.  
+    embed {{ tex-wrap-post ... }}.
 
   In addition, the program option -tex_wrap false can be used to omit
   wraping the tex output (-tex_wrap false overrides any
@@ -351,7 +347,6 @@ This version fixes a packaging problem of the version 0.21.
 
 - minor updates to the Hol backend to target the new Hol syntax.
 
-
 2012.01.04 fix for HOL multiple definitions bug
 
 2012.06.12 fix for HOL syntax change
@@ -360,39 +355,37 @@ This version fixes a packaging problem of the version 0.21.
 
 2012.12.04 bugfix  15158
 
-
-2013.04.20 
+2013.04.20
 
 - experimental support for generating Lem definitions, including new
   homs lem, lemvar, ichlo
 
-
-2013.06.22  
+2013.06.22
 
 - New aux-hom feature:
 
 We permit an aux hom on grammar rules. For any rule with such a hom,
 we transform that rule by appending an "_aux" to its primary nonterminal
 root name. We then add a synthesised rule with the original nonterminal
-root name and a single production, with a shape described by the body of 
-the aux hom, which must be of the form  
+root name and a single production, with a shape described by the body of
+the aux hom, which must be of the form
 
   {{ aux  foo1 foo2 _ bar1 bar2 bar3 }}
 
 with a single _ and any number of strings fooi and barj before and
 after, and no Raw_hom_ident's.  The _ is replaced by the original
-nonterminal root name.  
+nonterminal root name.
 
 For example, given a grammar or metavariable l of source locations, one
-might say 
+might say
 
 ntr :: 'NTR_'  ::=  {{ aux _ l }}
  | ...
 
-to synthesise grammars ntr_aux and ntr of unannotated and location-annotated 
-terms, the first with all the original productions and the second with a 
-single production 
- | ntr l :: :: NTR_aux. 
+to synthesise grammars ntr_aux and ntr of unannotated and location-annotated
+terms, the first with all the original productions and the second with a
+single production
+ | ntr l :: :: NTR_aux.
 
 If the rule has an empty production name wrapper (eg with '' in place
 of 'NTR_') then the production name is based on the original
@@ -405,7 +398,7 @@ for latex output and true for OCaml output.
 
 - New {{ texlong }} hom on productions, letting long productions
 be typeset with the production extending into the space usually used
-for comment, pushing that onto the next line. 
+for comment, pushing that onto the next line.
 
 2013.07.04
 
@@ -418,7 +411,7 @@ for comment, pushing that onto the next line.
 
 2013.10.24 Version 0.23
 
-2013.11.17 
+2013.11.17
 
 - add command-line option -output_source_locations <i>  to include
   comments in the output giving the source locations:
@@ -427,7 +420,7 @@ for comment, pushing that onto the next line.
     i=2 also adds a location for other components of the output
   Location annotations are lines of the form
 
-   (* #source file FILENAME1 lines M1 - N1  and ... and FILENAMEk lines Mk - Nk *) 
+   (* #source file FILENAME1 lines M1 - N1  and ... and FILENAMEk lines Mk - Nk *)
 
   (or with % instead of (* *) for the Latex output).
 
@@ -443,7 +436,7 @@ for comment, pushing that onto the next line.
 2016-10-27 Snapshot of 0.25 release moved to github at
             https://github.com/ott-lang/ott
 
-2017-02-10 Add command-line option -tex_suppress_category <string> to 
+2017-02-10 Add command-line option -tex_suppress_category <string> to
   suppress productions or rules with the specified category string.
 
 2017-02-13 Add command-line option -tex_suppress_ntr <string> to
@@ -452,7 +445,7 @@ for comment, pushing that onto the next line.
 2017-05-28 fixes for Coq 8.5 and 8.6, contributed by palmskog
 
 2017-05-29 - 2017-06-14  Add experimental support for generating a
-standalone lexer, menhir parser, and pretty printer, as illustrated in 
+standalone lexer, menhir parser, and pretty printer, as illustrated in
 tests/menhir_tests/test10menhir
 
 2017-07-17 fixes for OCaml safe string, contributed by jpdeplaix
@@ -475,7 +468,7 @@ tests/menhir_tests/test10menhir
 
 - improve menhir parser and pp generation for {{ phantom }} rules
 
-2017-10-11 
+2017-10-11
 
 - add highly experimental -aux_style_rules false option,
   adding aux info as extra constructor arguments rather than additional
@@ -493,7 +486,7 @@ tests/menhir_tests/test10menhir
 2017-11-27 Version 0.27
 
 2017-12-05 [Brian Campbell] Bugfix: add missing case of Lem auxparam type name
-hack when it's hom 
+hack when it's hom
 
 2018-01 [Peter Sewell, + palmskog for Coq] copy ocaml_light example
   sources from svn (rsem/ott/old_pre_github/examples/caml) and
@@ -581,3 +574,7 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l
 2024-12 @palmskog: only output plain comments in generated Coq code
 
 2024-12-30 Version 0.34
+
+2025-08-06 Version 0.xx
+
+2025-08 @SergioBenitez: Rocq 9.0 compatibility - update opam dependencies and CI workflow
diff --git a/src/bounds.ml b/src/bounds.ml
index 2959d16..6a19157 100644
--- a/src/bounds.ml
+++ b/src/bounds.ml
@@ -170,6 +170,84 @@ let split_bounded :
        f [] [] xbos
 
 
+(* Coalesce nonterminals with the same name and compatible bounds *)
+let coalesce_bounds xd loc x : ((nt_or_mv * subntr_data) * bound option) list =
+  (* Group by nonterminal name and suffix *)
+  let by_name_and_suffix = 
+    Auxl.remove_duplicates 
+      (List.map (fun (((ntmv, sf), _), _) -> (ntmv, sf)) x) 
+  in
+  
+  (* Get all entries for a given nonterminal and suffix *)
+  let entries_for ntmv sf = 
+    List.filter (fun (((nm, sf'), _), _) -> nm = ntmv && sf = sf') x 
+  in
+  
+  (* Check if two subntr_data are compatible *)
+  let compatible_subntr_data d1 d2 = match (d1, d2) with
+    | (None, _) | (_, None) -> true
+    | (Some (ntrl1, ntrt1), Some (ntrl2, ntrt2)) -> 
+        ntrl1 = ntrl2 && ntrt1 = ntrt2
+  in
+  
+  (* Check if two bounds are compatible *)
+  let compatible_bounds b1 b2 = match (b1, b2) with
+    | (None, _) | (_, None) -> true
+    | (Some b1, Some b2) -> b1 = b2
+  in
+  
+  (* Merge entries for a nonterminal *)
+  let merge_entries entries =
+    let rec find_best_entry remaining best =
+      match remaining with
+      | [] -> best
+      | entry :: rest ->
+          let (((_, _), sd), bo) = entry in
+          let (((_, _), best_sd), best_bo) = best in
+          
+          (* Prefer entries with subrule data over those without *)
+          let better = 
+            match sd, best_sd with
+            | Some _, None -> true
+            | None, Some _ -> false
+            | _, _ -> 
+                (* If both have or don't have subrule data, prefer those with bounds *)
+                match bo, best_bo with
+                | Some _, None -> true
+                | None, Some _ -> false
+                | _, _ -> false
+          in
+          
+          find_best_entry rest (if better then entry else best)
+    in
+    
+    match entries with
+    | [] -> failwith "Empty entries list in coalesce_bounds"
+    | first :: rest -> find_best_entry rest first
+  in
+  
+  (* Process each nonterminal and suffix pair *)
+  List.map (fun (ntmv, sf) -> 
+    let entries = entries_for ntmv sf in
+    
+    (* Check for incompatible entries *)
+    List.iter (fun e1 ->
+      List.iter (fun e2 ->
+        let ((_, sd1), bo1) = e1 in
+        let ((_, sd2), bo2) = e2 in
+        
+        if not (compatible_subntr_data sd1 sd2) then
+          raise (Bounds (loc, "incompatible subntr_data for nonterminal " ^ 
+                        (Grammar_pp.pp_nt_or_mv Types.pp_ascii_opts_default xd (ntmv, sf))))
+        else if not (compatible_bounds bo1 bo2) then
+          raise (Bounds (loc, "incompatible bounds for nonterminal " ^ 
+                        (Grammar_pp.pp_nt_or_mv Types.pp_ascii_opts_default xd (ntmv, sf))))
+      ) entries
+    ) entries;
+    
+    merge_entries entries
+  ) by_name_and_suffix
+
 (*invert, calculating, for each bound, the nt_or_mv that have that bound*)
 let nt_or_mv_per_bound :
  ((nt_or_mv*subntr_data) * bound ) list ->  (bound * (nt_or_mv*subntr_data) list) list 
@@ -325,7 +403,8 @@ let dotenv23 ntmvsn_without_bounds ntmvsn_with_bounds  =
 
 let bound_extraction m xd loc sts : dotenv * dotenv3 * string = 
   try  
-    let x = nt_or_mv_of_symterms sts in
+    let x_raw = nt_or_mv_of_symterms sts in
+    let x = coalesce_bounds xd loc x_raw in
     let bounds = check_length_consistency loc x in
     let pp_bounds = String.concat "  " 
         (List.map Grammar_pp.pp_plain_bound bounds) in
diff --git a/src/defns.ml b/src/defns.ml
index 90727f6..5a04aa9 100644
--- a/src/defns.ml
+++ b/src/defns.ml
@@ -258,7 +258,18 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit =
                   let ntr_upper = List.assoc ntr non_free_ntrs in
                   Some (ntr,ntr_upper,(ntr,suffix))
                 with
-                  Not_found -> None)
+                  Not_found -> 
+                    (* Try with the primary nonterminal to handle aliases *)
+                    let primary_ntr = 
+                      try Auxl.primary_ntr_of_ntr xd ntr 
+                      with Not_found -> ntr in
+                    if primary_ntr = ntr then None
+                    else
+                      try
+                        let ntr_upper = List.assoc primary_ntr non_free_ntrs in
+                        Some (primary_ntr,ntr_upper,(ntr,suffix))
+                      with
+                        Not_found -> None)
             | (Ntr ntr,suffix),Some(ntrl,ntru) -> Some (ntrl,ntru,(ntr,suffix))
             | (Mvr mvr,suffix),_ -> None) 
             ntmvsns in
diff --git a/src/grammar_typecheck.ml b/src/grammar_typecheck.ml
index 48c1b59..95e508d 100644
--- a/src/grammar_typecheck.ml
+++ b/src/grammar_typecheck.ml
@@ -1397,7 +1397,7 @@ let check_structure (xd:syntaxdefn) (str:structure) : unit =
 
 (** This constructs an internal representation of a grammar from a raw
     representation, typechecking the grammar on the way *)
-let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:bool) (targets:string list) (source_filenames:string list) (merge_fragments:bool)  (ris_per_file:raw_item list list)
+let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:bool) (targets:string list) (source_filenames:string list) (merge_fragments:bool) (skip_subrule_validation:bool) (ris_per_file:raw_item list list)
     : syntaxdefn * structure * raw_fun_or_reln_defnclass list =
 
   (* now we have in our hand the new ris_per_file that preserves the
@@ -2468,14 +2468,22 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b
 (*         else nodups xs ) in *)
 (*   nodups srs_lowers; *)
 
-  List.iter 
-    (fun sr -> ignore(subrule xd true sr.sr_lower sr.sr_upper)) xd.xd_srs;
+  (* Skip subrule validation if needed (for Menhir backend) *)
+  if not skip_subrule_validation then
+    List.iter 
+      (fun sr -> ignore(subrule xd true sr.sr_lower sr.sr_upper)) xd.xd_srs;
 
   (* as an internal consistency check, also check against the tops - should always succeed*)
   (* Further, record the production promotion maps *)
   let srd_subrule_pn_promotion = 
     List.map 
-      (fun sr -> (sr.sr_lower,(sr.sr_top,subrule xd true sr.sr_lower sr.sr_top))) xd.xd_srs in
+      (fun sr -> (sr.sr_lower,(sr.sr_top,
+        (* Skip subrule validation if needed (for Menhir backend) *)
+        if skip_subrule_validation then
+          (* Create dummy list for the case when validation is skipped *)
+          [(sr.sr_lower, sr.sr_top)]
+        else
+          subrule xd true sr.sr_lower sr.sr_top))) xd.xd_srs in
 
 
   let xd = {xd with xd_srd={xd.xd_srd with srd_subrule_pn_promotion=srd_subrule_pn_promotion}} in
diff --git a/src/grammar_typecheck.mli b/src/grammar_typecheck.mli
index 53d55c4..9edeed0 100644
--- a/src/grammar_typecheck.mli
+++ b/src/grammar_typecheck.mli
@@ -46,6 +46,7 @@ val check_and_disambiguate :
   Types.hom_name list ->
   string list ->
   bool ->
+  bool ->  (* skip_subrule_validation parameter *)
   Types.raw_item list list -> Types.syntaxdefn * Types.structure * Types.raw_fun_or_reln_defnclass list
 
 val check_with_parser :
diff --git a/src/lex_menhir_pp.ml b/src/lex_menhir_pp.ml
index d2989d5..949f450 100644
--- a/src/lex_menhir_pp.ml
+++ b/src/lex_menhir_pp.ml
@@ -111,9 +111,15 @@ let suppress_rule yo r =
   let suppressed_ntr = 
     List.mem r.rule_ntr_name yo.ppm_suppressed_ntrs
   in
+  (* Check if this nonterminal is non-maximal in the subrule hierarchy *)
+  let subrule_non_maximal =
+    match yo.syntaxdefn with
+    | None -> false (* If syntaxdefn is not available, don't suppress anything based on subrules *)
+    | Some xd -> List.exists (function sr -> sr.sr_lower = r.rule_ntr_name) xd.xd_srs
+  in
   [] = r.rule_ps (*List.filter (function p -> not (contains_list p)) r.rule_ps *)
 (*|| suppressed_ntr || (not(yo.ppm_show_meta) && r.rule_semi_meta) || r.rule_meta*)
-  || suppressed_ntr || r.rule_semi_meta
+  || suppressed_ntr || r.rule_semi_meta || subrule_non_maximal
 
 
 (* tokens arise from terminals and metavardefns *)
@@ -916,11 +922,11 @@ let pp_pp_raw_metavar_defn yo generate_aux_info xd ts md =
         | Some [Hom_string s] when s="string" -> 
            Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string \"\\\"\" ^^ string " ^ svi ^ " ^^ string \"\\\"\"\n\n")
         | Some [Hom_string s] when s="int" -> 
-           Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string_of_int " ^ svi ^ "\n\n")
+           Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string (string_of_int " ^ svi ^ ")\n\n")
         | Some [Hom_string s] when s="big_int" -> 
-           Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " Big_int.string_of_big_int " ^ svi ^ "\n\n")
+           Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string (Big_int.string_of_big_int " ^ svi ^ ")\n\n")
         | Some [Hom_string s]  -> 
-           Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string_of_" ^ s ^ " " ^ svi ^ "\n\n")
+           Some (pp_pp_raw_name md.mvd_name ^ " "^svi^" = " ^ " string (string_of_" ^ s ^ " " ^ svi ^ ")\n\n")
         | Some hs -> Some ("no default for "^md.mvd_name^" ocaml homspec="^Grammar_pp.pp_plain_hom_spec hs ^ "\n\n")
         | None -> Some ("no pp-raw or ocaml hom for "^md.mvd_name^ "\n\n")
        )
@@ -941,11 +947,11 @@ let pp_pp_metavar_defn yo generate_aux_info xd ts md =
         | Some [Hom_string s] when s="string" -> 
            Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string " ^ svi ^ " ^^ string \"\"\n\n")
         | Some [Hom_string s] when s="int" -> 
-           Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string_of_int " ^ svi ^ "\n\n")
+           Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string (string_of_int " ^ svi ^ ")\n\n")
         | Some [Hom_string s] when s="big_int" -> 
-           Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ " Big_int.string_of_big_int " ^ svi ^ "\n\n")
+           Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string (Big_int.string_of_big_int " ^ svi ^ ")\n\n")
         | Some [Hom_string s]  -> 
-           Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ " string_of_" ^ s ^ " " ^ svi ^ "\n\n")
+           Some (pp_pp_name md.mvd_name ^ " "^svi^" = " ^ "string (string_of_" ^ s ^ " " ^ svi ^ ")\n\n")
         | Some hs -> Some ("no pp default for "^md.mvd_name^" ocaml homspec="^Grammar_pp.pp_plain_hom_spec hs ^ "\n\n")
         | None -> Some ("no pp or ocaml hom for "^md.mvd_name^ "\n\n")
        )
@@ -1194,7 +1200,10 @@ let pp_menhir_precedences fd ts =
 *)
 
 (* output a menhir source file *)
-let pp_menhir_syntaxdefn m sources _(*xd_quotiented*) xd_unquotiented lookup generate_aux_info oi = let yo = match m with Menhir yo -> yo | _ -> raise (Failure "pp_menhir_systemdefn called with bad ppmode") in 
+let pp_menhir_syntaxdefn m sources _(*xd_quotiented*) xd_unquotiented lookup generate_aux_info oi = 
+  let yo = match m with Menhir yo -> yo | _ -> raise (Failure "pp_menhir_systemdefn called with bad ppmode") in 
+  (* Store the syntax definition for use in rule suppression decisions *)
+  yo.syntaxdefn <- Some xd_unquotiented;
   match oi with
   | (o,is)::[] ->
       let _ = Auxl.filename_check m o in
diff --git a/src/main.ml b/src/main.ml
index 0c67e50..caa120f 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -488,6 +488,7 @@ let yo = {
                  ppm_caml_opts = oo;
                  ppm_caml_ast_module = target_ocaml_ast_module;
                  ppm_caml_parser_module = target_ocaml_parser_module;
+                 syntaxdefn = None;
  }
 
 let m_menhir = Menhir yo 
@@ -612,9 +613,9 @@ let process source_filenames =
 
   (* the quotiented un-auxed syntax, used to generate the pp functions, should be without the generated aux rules *)
 
-  let f quotient generate_aux = 
+  let f quotient generate_aux skip_validation = 
     try 
-      Grammar_typecheck.check_and_disambiguate m_tex quotient generate_aux targets_non_tex (List.map snd source_filenames) (!merge_fragments) document 
+      Grammar_typecheck.check_and_disambiguate m_tex quotient generate_aux targets_non_tex (List.map snd source_filenames) (!merge_fragments) skip_validation document 
     with
     | Typecheck_error (loc,s1,s2) ->
         Auxl.error (Some loc) ("(in checking and disambiguating "^(if quotient then "quotiented " else "") ^ "syntax)\n"^s1
@@ -622,11 +623,15 @@ let process source_filenames =
                     ^ "\n")
   in
 
+  let menhir_target = List.mem "menhir" targets in
+
   let ((xd,structure,rdcs),xd_unquotiented,xd_quotiented_unaux) = 
-    if List.mem "menhir" targets (*|| !caml_pp_filename <> None*) then 
-      (f true !generate_aux_rules, (match f false false with (xd,_,_)-> xd), (match f !generate_aux_rules false with (xd,_,_)-> xd))
+    if menhir_target (*|| !caml_pp_filename <> None*) then 
+      (f true !generate_aux_rules false, 
+       (match f false false menhir_target with (xd,_,_)-> xd), 
+       (match f !generate_aux_rules false false with (xd,_,_)-> xd))
     else
-      match f !quotient_rules !generate_aux_rules with 
+      match f !quotient_rules !generate_aux_rules false with 
       | (xd,structure,rdcs) -> ((xd,structure,rdcs), xd, xd (* two dummies, unused *))
   in
 
diff --git a/src/subrules_pp.ml b/src/subrules_pp.ml
index 002ccec..5638bb0 100644
--- a/src/subrules_pp.ml
+++ b/src/subrules_pp.ml
@@ -117,30 +117,37 @@ let pp_subrules m xd srs : int_funcs_collapsed =
   let rec pp_subelement = 
     fun sie de isa_list_name_flag pu srl sru el eu -> match el,eu with
       Lang_nonterm (ntrpl,ntl), Lang_nonterm (ntrpu,ntu) -> 
-        (* TODO: THIS IS PROBABLY WRONG WRONG WRONG *)
-(*         if  (ntrpl=ntrpu) then  *)
-(*           try  *)
-(*             let ntr_upper = List.assoc ntrpl non_free_ntrs in *)
-(*             [ "(" ^ (Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)) ^ " "  *)
-(*               ^ Grammar_pp.pp_nonterm_with_sie m xd sie ntu  *)
-(* 	      ^ ")"], [Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)], [] *)
-(*           with Not_found -> [],[],[] *)
-(*         else if  *)
-(*           List.exists  *)
-(*             (function sr -> sr.sr_lower=ntrpl && sr.sr_upper=ntrpu)  *)
-(*             xd.xd_srs  *)
-(*         then  *)
-(*           [ "(" ^ (Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)) ^ " "  *)
-(*             ^ Grammar_pp.pp_nonterm_with_sie m xd sie ntu ^")"],  *)
-(*           [Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)], [] *)
-(*         else [],[],[] *)
-
-        (try
-          let ntr_upper = List.assoc ntrpl non_free_ntrs in
-          [ "(" ^ (Auxl.pp_is ntrpl ntr_upper) ^ " " 
+        (* Check if there's a direct subrule relationship, checking both the nonterminal
+           and its primary form to handle alias cases *)
+        let direct_subrule = 
+          let primary_ntrpl = 
+            try Auxl.primary_ntr_of_ntr xd ntrpl 
+            with Not_found -> ntrpl in
+          List.exists 
+            (function sr -> 
+              (sr.sr_lower=ntrpl || sr.sr_lower=primary_ntrpl) && 
+              sr.sr_upper=ntrpu)
+            xd.xd_srs
+        in
+        
+        if direct_subrule then
+          [ "(" ^ (Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)) ^ " " 
             ^ Grammar_pp.pp_nonterm_with_sie m xd sie ntu 
-	    ^ ")"], [Auxl.pp_is ntrpl ntr_upper], []
-        with Not_found -> [],[],[])
+            ^ ")"], [Auxl.pp_is ntrpl (Auxl.promote_ntr xd ntrpu)], []
+        else
+          (* Try to find the top-level nonterminal for this subrule *)
+          (try
+            let primary_ntrpl = 
+              try Auxl.primary_ntr_of_ntr xd ntrpl 
+              with Not_found -> ntrpl in
+            let ntr_upper = 
+              try List.assoc ntrpl non_free_ntrs 
+              with Not_found -> List.assoc primary_ntrpl non_free_ntrs in
+            let promoted_upper = Auxl.promote_ntr xd ntr_upper in
+            [ "(" ^ (Auxl.pp_is ntrpl promoted_upper) ^ " " 
+              ^ Grammar_pp.pp_nonterm_with_sie m xd sie ntu 
+              ^ ")"], [Auxl.pp_is ntrpl promoted_upper], []
+          with Not_found -> [],[],[])
 
     | Lang_metavar _, Lang_metavar _ -> [],[],[]
     | Lang_terminal _, Lang_terminal _ -> [],[],[]
diff --git a/src/system_pp.ml b/src/system_pp.ml
index 88f3b2e..409df78 100644
--- a/src/system_pp.ml
+++ b/src/system_pp.ml
@@ -33,7 +33,6 @@
 
 open Types;;
 
-
 (* Print auxiliary lemmas if necessary *)
 
 let rec uses_lists_element e =
@@ -351,6 +350,12 @@ let pp_systemdefn_core fd m sd lookup =
       end
   | _ -> () )
 
+(* Helper function to format Require Import statements with From Coq prefix for stdlib *)
+let format_require_import th =
+  match th with
+  | "Arith" | "Bool" | "List" -> "From Coq Require Import " ^ th ^ "."
+  | _ -> "Require Import " ^ th ^ "."
+
 (* old algorithm, used only when pp with -merge true *)
 let pp_systemdefn fd m sd lookup fn =
 
@@ -384,14 +389,14 @@ let pp_systemdefn fd m sd lookup fn =
       then begin
         Printf.fprintf fd "(* generated by Ott %s, locally-nameless %sfrom: %s *)\n"
           Version.n (if Auxl.is_lngen m then "lngen " else "") sd.sources;
-        List.iter (fun th -> Printf.fprintf fd "Require Import %s.\n" th) 
+        List.iter (fun th -> Printf.fprintf fd "%s\n" (format_require_import th)) 
 			( match co.coq_expand_lists with
 			| true -> ["Metalib.Metatheory"]
 			| false -> ["Bool"; "Metalib.Metatheory"; "List"; "Ott.ott_list_core"])
 
       end else begin
         Printf.fprintf fd "(* generated by Ott %s from: %s *)\n" Version.n sd.sources;
-        List.iter (fun th -> Printf.fprintf fd "Require Import %s.\n" th) 
+        List.iter (fun th -> Printf.fprintf fd "%s\n" (format_require_import th)) 
                      ( match co.coq_expand_lists with
                      | true -> ["Arith"; "Bool"; "List"]
                      | false -> ["Arith"; "Bool"; "List"; "Ott.ott_list_core"])
@@ -433,7 +438,7 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments =
         let fd = open_out o in
         Printf.fprintf fd "(* generated by Ott %s, locally-nameless %sfrom: %s *)\n"
           Version.n (if Auxl.is_lngen m then "lngen " else "") sd.sources;
-        List.iter (fun th -> Printf.fprintf fd "Require Import %s.\n" th) 
+        List.iter (fun th -> Printf.fprintf fd "%s\n" (format_require_import th)) 
 			( match co.coq_expand_lists with
 			| true -> ["Metalib.Metatheory"]
 			| false -> ["Bool"; "Metalib.Metatheory"; "List"; "Ott.ott_list_core"]);
@@ -476,7 +481,7 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments =
            | Coq co ->
                [ Embed_string (dummy_loc,
 	           "(* generated by Ott " ^ Version.n ^ " from: " ^ file_sources ^ " *)\n\n"
-	           ^ String.concat "\n" (List.map (fun th -> "Require Import " ^ th ^ ".") 
+	           ^ String.concat "\n" (List.map format_require_import 
 				           ( match co.coq_expand_lists with
 				           | true -> ["Arith"; "Bool"; "List"]
 				           | false -> ["Arith"; "Bool"; "List"; "Ott.ott_list_core"]))
diff --git a/src/types.ml b/src/types.ml
index f770b73..4987295 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -854,6 +854,7 @@ type pp_menhir_opts =
       ppm_caml_opts : pp_caml_opts; 
       ppm_caml_ast_module : string;
       ppm_caml_parser_module : string;
+      mutable syntaxdefn : syntaxdefn option;
     } (* yo *)
 type pp_yacc_opts = unit (* yo *)
 
diff --git a/tests/menhir_tests/test10menhir/test10menhir.ott b/tests/menhir_tests/test10menhir/test10menhir.ott
index 616bfaf..7909dae 100644
--- a/tests/menhir_tests/test10menhir/test10menhir.ott
+++ b/tests/menhir_tests/test10menhir/test10menhir.ott
@@ -7,18 +7,22 @@
 
 % - tex for the quotiented grammar
 
-metavar var, x ::=   {{ com  term variable }} 
+% ensure we generate correct parses for int / float / bool
+metavar boolean ::= {{ ocaml bool }} {{ coq nat }}
+metavar integer ::= {{ ocaml int }} {{ coq nat }}
+metavar floating ::= {{ ocaml float }} {{ coq nat }}
+
+metavar var, x ::=   {{ com  term variable }}
 {{ isa string}} {{ coq nat}} {{ hol string}} {{ lem string }} {{ coq-equality }}
 {{ ocaml string}} {{ lex alphanum}} {{ tex \mathit{[[var]]} }} {{ ocamllex ['a'-'z''A'-'Z']+ }}
 
 grammar
 %                lhs_of_app  rhs_of_app  lambda_body
-%  | ( t )           y          y            y 
+%  | ( t )           y          y            y
 %  | x               y          y            y
 %  | \ x . t         n          y            y
 %  | t t'            y          n            y
 
-
 term, t, v :: 'T_' ::=               {{ menhir-start }}
   | at             :: :: at          {{ quotient-remove }}   {{ ocaml [[at]] }}
   | lhs rhs'       :: :: app
@@ -26,21 +30,20 @@ term, t, v :: 'T_' ::=               {{ menhir-start }}
 
   | { t / x } t' :: M :: sub         {{ ichlo (tsubst_term [[t]] [[x]] [[t']])}}
 
-                   
-atomic_term, at :: 'T_' ::=       {{ quotient-with t }}      
+atomic_term, at :: 'T_' ::=       {{ quotient-with t }}
   | x              :: :: var
   | ( t )          :: :: paren
-                   
-lhs :: 'T_' ::=                   {{ quotient-with t }}      
+
+lhs :: 'T_' ::=                   {{ quotient-with t }}
   | at             :: :: at_lhs       {{ quotient-remove }}   {{ ocaml [[at]] }}
   | lhs at'        :: :: app_lhs      {{ quotient-remove }}   {{ ocaml T_app([[lhs]], [[at']]) }}
-                   
-rhs :: 'T_' ::=                   {{ quotient-with t }}      
+
+rhs :: 'T_' ::=                   {{ quotient-with t }}
   | at             :: :: at_rhs       {{ quotient-remove }}   {{ ocaml [[at]] }}
   | lambda         :: :: fn_rhs       {{ quotient-remove }}   {{ ocaml [[lambda]] }}
-                   
+
 lambda :: 'T_' ::=                {{ quotient-with t }}
-  | \ x . t        :: :: lambda   
+  | \ x . t        :: :: lambda
 
 % in principle, these ocaml homs, which are used in the parser actions
 % of the removed productions, could be constructed automatically, by
@@ -49,10 +52,9 @@ lambda :: 'T_' ::=                {{ quotient-with t }}
 % nonterminal roots.  Neither seems worth the complexity right now,
 % though.
 
-
 % the parser generation code doesn't currently support subrules
 
-% %val,v :: 'v_' ::=                            {{ com value   }} 
+% %val,v :: 'v_' ::=                            {{ com value   }}
 % %  | \ x . t      ::   :: lam                   {{ com lambda  }}
 
 terminals :: 'terminals_' ::=
@@ -63,24 +65,22 @@ terminals :: 'terminals_' ::=
 %  val <:: term
 
 % substitutions
-%   single term var :: tsubst 
-% 
+%   single term var :: tsubst
+%
 %  defns
 %  Jop :: '' ::=
-%  
+%
 %   defn
 %   t1 --> t2 :: ::reduce::'' {{ com [[t1]] reduces to [[t2]] }} {{ lemwcf  witness type reduce_witness; check reduce_check; eval : input -> output }} by
-%  
-%  
+%
+%
 %      --------------------------  :: ax_app
 %      (\x.t1) v2 -->  {v2/x}t1
-%  
+%
 %      t1 --> t1'
 %      -------------- :: ctx_app_fun
 %      t1 t --> t1' t
-%  
+%
 %      t1 --> t1'
 %      -------------- :: ctx_app_arg
 %      v t1 --> v t1'
-
-
diff --git a/tests/menhir_tests/test_subrules/Makefile b/tests/menhir_tests/test_subrules/Makefile
new file mode 100644
index 0000000..24d4d84
--- /dev/null
+++ b/tests/menhir_tests/test_subrules/Makefile
@@ -0,0 +1,47 @@
+#  make -C ../.. && make clean && make
+
+ROOT            := test_subrules
+
+OTTDIR          := ../../..
+
+OTT             := $(OTTDIR)/bin/ott
+
+MENHIR_EXTRA_LIB:= $(OTTDIR)/menhir/menhir_library_extra.mly
+
+MENHIR          := menhir
+
+MENHIRFLAGS     := --infer --explain --unused-tokens --trace --base $(ROOT)_parser
+
+OCAMLBUILD      := ocamlbuild -use-ocamlfind -package pprint \
+				   -use-menhir -menhir "$(MENHIR) $(MENHIRFLAGS) ../$(MENHIR_EXTRA_LIB) "
+
+MAIN            := main
+
+all: $(ROOT)_ast.ml $(ROOT)_parser.mly $(ROOT)_parser_pp.ml $(ROOT)_lexer.mll main.ml
+	$(OCAMLBUILD) $(MAIN).byte
+
+pdf: $(ROOT)_quotiented.pdf $(ROOT)_unquotiented.pdf
+
+# generate the ocaml AST type, ocamllex lexer, menhir parser, and ocaml pretty printers for the AST, all from the Ott soruce
+$(ROOT)_ast.ml  $(ROOT)_lexer.mll $(ROOT)_parser.mly $(ROOT)_parser_pp.ml $(ROOT)_ast.tex : $(ROOT).ott
+	$(OTT) -show_sort true -quotient_rules false -i $(ROOT).ott  -o $(ROOT)_parser.mly -o $(ROOT)_lexer.mll -o $(ROOT)_ast.ml -o $(ROOT).tex
+
+$(ROOT)_quotiented.pdf: $(ROOT).ott Makefile
+	$(OTT) -quotient_rules true -i $(ROOT).ott -o $(ROOT)_quotiented.tex
+	pdflatex $(ROOT)_quotiented.tex
+
+$(ROOT)_unquotiented.pdf: $(ROOT).ott Makefile
+	$(OTT) -quotient_rules false -i $(ROOT).ott -o $(ROOT)_unquotiented.tex
+	pdflatex $(ROOT)_unquotiented.tex
+
+clean:
+	rm -rf *~
+	rm -rf _build
+	rm -rf $(ROOT)_ast.ml $(ROOT)_parser.mly $(ROOT)_lexer.mll $(ROOT)_parser_pp.ml
+	rm -rf *.aux *.log *.tex
+	rm -rf main.native main.byte
+	$(OCAMLBUILD) -clean
+
+realclean:
+	$(MAKE) clean
+	rm -rf *.pdf
diff --git a/tests/menhir_tests/test_subrules/main.ml b/tests/menhir_tests/test_subrules/main.ml
new file mode 100644
index 0000000..fb6c2cd
--- /dev/null
+++ b/tests/menhir_tests/test_subrules/main.ml
@@ -0,0 +1,27 @@
+open Test_subrules_ast
+
+module Lexer = Test_subrules_lexer
+module Parser = Test_subrules_parser
+module PP = Test_subrules_parser_pp
+
+let process (line : string) =
+  let linebuf = Lexing.from_string line in
+  try
+    (* Run the parser on this line of input. *)
+    let t = (Parser.expr_start Lexer.token linebuf) in
+    Printf.printf "   "; PPrint.ToChannel.compact stdout (PP.pp_raw_expr t); Printf.printf "\n";
+    Printf.printf "   "; PPrint.ToChannel.compact stdout (PP.pp_expr t); Printf.printf "\n"
+  with
+  | Lexer.Error msg ->
+      Printf.fprintf stdout "%s" msg
+  | Parser.Error ->
+      Printf.fprintf stdout "%s^\nAt offset %d: syntax error.\n" (String.make (Lexing.lexeme_start linebuf) ' ') (Lexing.lexeme_start linebuf)
+
+let () = Printf.printf "Enter a Test_subrules expression:\n"
+
+let rec run () =
+  let s = read_line () in
+  process s; flush stdout;
+  run ()
+
+let () = run ()
diff --git a/tests/menhir_tests/test_subrules/test_subrules.ott b/tests/menhir_tests/test_subrules/test_subrules.ott
new file mode 100644
index 0000000..42ee7ce
--- /dev/null
+++ b/tests/menhir_tests/test_subrules/test_subrules.ott
@@ -0,0 +1,37 @@
+metavar nat, k ::=
+  {{ com natural numbers }}
+  {{ lex numeral }}
+  {{ coq nat }}
+  {{ ocaml int }}
+  {{ ocamllex ['0'-'9']+ }}
+
+grammar
+
+num :: 'num_' ::= {{ com num }} {{ pp-suppress }} {{ menhir-start }}
+  | k           ::   :: int   {{ com integer }}
+
+value, v  :: 'value_' ::= {{ com value }} {{ pp-suppress }} {{ menhir-start }}
+  | k           ::   :: int   {{ com integer }}
+  | ( v1 , v2 ) ::   :: tuple {{ com tuple }}
+
+expr, e  :: 'expr_' ::= {{ com expression }} {{ menhir-start }}
+  | term        ::   :: term  {{ com term }} {{ quotient-remove }} {{ ocaml [[term]] }}
+  | e1 + e2     ::   :: add   {{ com addition }}
+
+term :: 'expr_' ::= {{ com term }} {{ quotient-with expr }}
+  | k           ::   :: int   {{ com integer }}
+  | term . k    ::   :: proj  {{ com projection }}
+  | ( e1 , e2 ) ::   :: tuple {{ com tuple }}
+  | ( e )       :: S :: paren {{ icho [[e]] }}
+
+parsing
+
+expr_add left expr_add
+
+embed {{ menhir %left PLUS }}
+
+% this is what we're testing, to ensure we have minimal support for subrules. we
+% should only take the maximal elements from the subrule order: `e` in this case
+subrules
+  v <:: e
+  num <:: v
diff --git a/tests/test21.1.ott b/tests/test21.1.ott
index 25f6ed9..70c34d9 100644
--- a/tests/test21.1.ott
+++ b/tests/test21.1.ott
@@ -1,42 +1,47 @@
 metavar n ::=
+  {{ lex numeral }} {{ coq nat }}
 
 grammar
 
-e :: e_ ::= 
-| n             ::   :: num
-| - e           ::   :: neg
-| e1 + e2       ::   :: add
-| e1 - e2       ::   :: sub
-| e1 e2         ::   :: mul
-| e1 / e2       ::   :: div
-| e1 , .. , e2  ::   :: tup
-| ( e )         :: M :: par {{ icho [[e]] }}
+e :: e_ ::=
+  | n                ::   :: num
+  | - e              ::   :: neg
+  | e1 + e2          ::   :: add
+  | e1 - e2          ::   :: sub
+  | e1 * e2          ::   :: mul
+  | e1 / e2          ::   :: div
+  | ( e1 , .. , e2 ) ::   :: tup
 
 parsing
 
-e_add left e_add   % #1
-e_sub left e_sub
-e_add left e_sub   % #3
-e_sub left e_add
-
-e_mul left e_mul
-e_div left e_div
-e_mul left e_div
-e_div left e_mul
-
-e_neg <= e_add     % #9
-e_neg <= e_sub
-e_neg <= e_mul
-e_neg <= e_div
-e_neg <= e_tup
-
-e_add <= e_div
-e_add <= e_mul     % #15
-e_add <= e_tup
-e_sub <= e_div
-e_sub <= e_mul
-e_sub <= e_tup
-
-e_mul <= e_tup     % #20
-e_div <= e_tup
-
+  e_add left e_add   % #1
+  e_sub left e_sub
+  e_add left e_sub   % #3
+  e_sub left e_add
+
+  e_mul left e_mul
+  e_div left e_div
+  e_mul left e_div
+  e_div left e_mul
+
+  e_add <= e_neg     % #9
+  e_sub <= e_neg
+  e_mul <= e_neg
+  e_div <= e_neg
+  e_tup <= e_neg
+
+  e_add <= e_div
+  e_add <= e_mul     % #15
+  e_add <= e_tup
+  e_sub <= e_div
+  e_sub <= e_mul
+  e_sub <= e_tup
+
+  e_mul <= e_tup     % #20
+  e_div <= e_tup
+
+defns tester :: T ::=
+  defn e :: :: red :: E_ {{ com Evaluation }} by
+
+  --------------- :: Test
+  -1 + 2 - 3 * 4
diff --git a/tests/test_lists_coq_defn_subrule_4.ott b/tests/test_lists_coq_defn_subrule_4.ott
new file mode 100644
index 0000000..0b2bf2a
--- /dev/null
+++ b/tests/test_lists_coq_defn_subrule_4.ott
@@ -0,0 +1,79 @@
+% Mixing list bounds with subrules
+% Should pass on all targets, but previous versions failed
+% in Coq with "The variable tau_ is bound several times in pattern"
+% due to an error in how bound were calculated for sub-non-terminals
+
+metavar var, X ::= {{ coq nat }}
+
+indexvar n ::=  {{ coq nat }}
+
+grammar
+
+Kind, K :: kind_ ::=
+  | KindStar ::  :: KindStar
+
+typexpr, T :: T_ ::=
+  | X                                    ::   :: var
+  | ForAll << X1 , .. , Xn >> .  T       ::   :: polyarrow
+  | [ X1 |-> tau1 .. Xn |-> taun ] T     :: M :: tsub  {{ icho  [[T]] }}
+
+tau, t :: tau_ ::=
+  | X  ::   :: var
+
+formula :: 'formula_' ::=
+  | judgement            ::   :: judgement
+  | formula1 .. formulan ::   :: dots
+
+subrules
+  tau <:: T
+
+defns
+  Jtype :: '' ::=
+
+defn
+  |- t : K :: :: kind :: Kind
+by
+
+  ------------------------------------ :: Var
+  |- t : KindStar
+
+defn
+  is t ::  :: Simpl :: ''
+by
+
+  ------------------------------------ :: Basic
+  is X
+
+defn
+  |- T <: T' :: :: sub :: Sub
+by
+
+  </ |-  taun : KindStar // n />
+  ------------------------------------------ :: InstL
+  |-  ForAll << </ Xn // n /> >> .  T  <: [ </ Xn |-> taun // n /> ] T
+
+  is t
+  ------------------------------------------ :: Sub
+  |- t <: X
+
+embed {{ coq
+
+Require Import List.
+Import ListNotations.
+
+Lemma test_is_tau_premise_needed :
+  (sub (T_polyarrow nil (T_var 0)) (T_var 1)) -> Is_true (is_tau_of_typexpr (T_polyarrow [] (T_var 0))).
+Proof.
+  intros.
+  inversion H.
+  assumption.
+Qed.
+
+Theorem is_tau_required_for_kind :
+  forall t, kind t kind_KindStar -> Is_true (is_tau_of_typexpr t).
+Proof.
+  intros.
+  inversion H.
+  assumption.
+Qed.
+}}