diff options
| author | Michael Soegtrop | 2020-07-05 07:49:37 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2020-07-05 07:49:37 +0200 |
| commit | 0545c9402310efe0656793197c996d04d554ecb8 (patch) | |
| tree | a7ee9471b02a4cad3f87a241299decb36bc935f7 | |
| parent | 99889823890c9d414335dc25df8f30ae06575f94 (diff) | |
| parent | 810197a6577c7a4a40f406ae64f918f72e7d0012 (diff) | |
Merge PR #12594: Fix ltac2 type parameters
Reviewed-by: MSoegtropIMC
Reviewed-by: gares
| -rw-r--r-- | doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst | 5 | ||||
| -rw-r--r-- | test-suite/ltac2/syntax.v | 12 | ||||
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 10 |
3 files changed, 24 insertions, 3 deletions
diff --git a/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst new file mode 100644 index 0000000000..555020d319 --- /dev/null +++ b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Fix the parsing of multi-parameters Ltac2 types + (`#12594 <https://github.com/coq/coq/pull/12594>`_, + fixes `#12595 <https://github.com/coq/coq/issues/12595>`_, + by Pierre-Marie Pédrot). diff --git a/test-suite/ltac2/syntax.v b/test-suite/ltac2/syntax.v new file mode 100644 index 0000000000..872b2142d0 --- /dev/null +++ b/test-suite/ltac2/syntax.v @@ -0,0 +1,12 @@ +Require Import Ltac2.Ltac2. + +Ltac2 Type ('a, 'b, 'c) t. +Ltac2 Type ('a) u. +Ltac2 Type 'a v. + +Ltac2 foo + (f : ('a, 'b, 'c) t -> ('a -> 'a, 'b -> 'c, 'c * 'c) t) + (x : ('a, 'b, 'c) t) := + f x. + +Ltac2 bar (x : 'a u) (y : ('b) v) := x. diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 3af39ec59a..bec9632e84 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -262,12 +262,16 @@ GRAMMAR EXTEND Gram | "1" LEFTA [ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ] | "0" - [ "("; t = tac2type LEVEL "5"; ")" -> { t } + [ "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid -> + { match p, qid with + | [t], None -> t + | _, None -> CErrors.user_err ~loc (Pp.str "Syntax error") + | ts, Some qid -> CAst.make ~loc @@ CTypRef (RelId qid, p) + } | id = typ_param -> { CAst.make ~loc @@ CTypVar (Name id) } | "_" -> { CAst.make ~loc @@ CTypVar Anonymous } | qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) } - | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid -> - { CAst.make ~loc @@ CTypRef (RelId qid, p) } ] + ] ]; locident: [ [ id = Prim.ident -> { CAst.make ~loc id } ] ] |