diff options
| author | delahaye | 2002-03-19 04:30:46 +0000 |
|---|---|---|
| committer | delahaye | 2002-03-19 04:30:46 +0000 |
| commit | fae65d853f23ed17c3ec9840dabb2e77551dc14b (patch) | |
| tree | f5fe23295d27aede5d34bd002827f1473bac529f | |
| parent | 0c690c0b517f8becbd0a61a68a43b30ea1da1380 (diff) | |
Ajout de l'entrée ne_constrarg_list
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2543 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |