Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.

4 files changed, 26 insertions, 13 deletions

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 53b726432..ec3a49df4 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause
 | [ in_clause'(cl) ] -> [ cl ]
 END
 
+let local_test_lpar_id_colon =
+  let err () = raise Stream.Failure in
+  Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+    (fun strm ->
+      match Util.stream_nth 0 strm with
+        | Tok.KEYWORD "(" ->
+            (match Util.stream_nth 1 strm with
+              | Tok.IDENT _ ->
+                  (match Util.stream_nth 2 strm with
+                    | Tok.KEYWORD ":" -> ()
+                    | _ -> err ())
+              | _ -> err ())
+        | _ -> err ())
+
+let pr_lpar_id_colon _ _ _ _ = mt ()
+
+ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
+| [ local_test_lpar_id_colon(x) ] -> [ () ]
+END
+
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
 let pr_r_nat_field natf =
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 7d4bccfad..9b4167512 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -67,6 +67,10 @@ val pr_by_arg_tac :
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
 
+val test_lpar_id_colon : unit Pcoq.Gram.entry
+
+val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
+
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 3e6ccaf84..bd48614db 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -463,7 +463,7 @@ open Evar_tactics
 (* TODO: add support for some test similar to g_constr.name_colon so that
    expressions like "evar (list A)" do not raise a syntax error *)
 TACTIC EXTEND evar
-  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
+  [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 4b3ca80af..e33c25cf8 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq =
         | _ -> err ())
 
 (* idem for (x:t) *)
-let test_lpar_id_colon =
-  Gram.Entry.of_parser "lpar_id_colon"
-    (fun strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =