aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-15 10:46:15 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-15 11:58:21 +0100
commit003fe3d5e60b8d89b28e718e3d048818caceb56a (patch)
tree34d21c56940b9ff18046633486d6d12d121301ad /parsing/pcoq.mli
parentfa0b0bedf165812b170cedbce8a5b6cf94a5fadf (diff)
Adding a token "index" representing positions (1st, 2nd, etc.).
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r--parsing/pcoq.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c224dbad9..ad4d9e501 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -173,6 +173,7 @@ module Prim :
val pattern_identref : Id.t located Gram.entry
val base_ident : Id.t Gram.entry
val natural : int Gram.entry
+ val index : int Gram.entry
val bigint : Bigint.bigint Gram.entry
val integer : int Gram.entry
val string : string Gram.entry