aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml4
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-16 10:16:00 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-16 10:16:00 +0000
commit436dd248125d3aca29755be16c146dd9b2732c88 (patch)
tree17e58b8927d4c9029ed5da956ec8edc808e4d808 /parsing/pcoq.ml4
parentadca2532e06efc6b66ed489cf1d8f778fdee2cea (diff)
Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewrite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1133 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pcoq.ml4')
-rw-r--r--parsing/pcoq.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 4fba8e891..fbbec9b34 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -349,6 +349,7 @@ module Vernac =
let ne_identarg_list = gec_list "ne_identarg_list"
let qualidarg = gec "qualidarg"
let qualidconstarg = gec "qualidconstarg"
+ let ne_qualidarg_list = gec_list "ne_qualidarg_list"
let numarg = gec "numarg"
let numarg_list = gec_list "numarg_list"
let ne_numarg_list = gec_list "ne_numarg_list"