diff options
| -rw-r--r-- | parsing/g_tactic.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
3 files changed, 5 insertions, 0 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 5c11995503..f3b4d2f170 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -182,6 +182,9 @@ GEXTEND Gram constrarg_list: [ [ c = constrarg; l = constrarg_list -> c :: l | -> [] ] ] ; + ne_constrarg_list: + [ [ c = constrarg; l = constrarg_list -> c :: l ] ] + ; unfold_occ: [ [ nl = LIST1 pure_numarg; c = qualidarg -> <:ast< (UNFOLD $c ($LIST $nl)) >> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index c45c8227d6..407bec37fc 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -292,6 +292,7 @@ module Tactic = let numarg_binding_list = gec_list "numarg_binding_list" let lconstrarg_binding_list = gec_list "lconstrarg_binding_list" let constrarg_list = gec_list "constrarg_list" + let ne_constrarg_list = gec_list "ne_constrarg_list" let ident_or_numarg = gec "ident_or_numarg" let ident_or_constrarg = gec "ident_or_constrarg" let identarg = gec "identarg" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 781c651621..b9317f5813 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -113,6 +113,7 @@ module Tactic : val constrarg : Coqast.t Gram.Entry.e val constrarg_binding_list : Coqast.t list Gram.Entry.e val constrarg_list : Coqast.t list Gram.Entry.e + val ne_constrarg_list : Coqast.t list Gram.Entry.e val fixdecl : Coqast.t list Gram.Entry.e val ident_or_numarg : Coqast.t Gram.Entry.e val ident_or_constrarg : Coqast.t Gram.Entry.e |