aboutsummaryrefslogtreecommitdiff
path: root/intf/constrexpr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/constrexpr.mli')
-rw-r--r--intf/constrexpr.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 79f4e99e1f..6543db6a17 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -32,7 +32,9 @@ type abstraction_kind = AbsLambda | AbsPi
type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
-type prim_token = Numeral of Bigint.bigint | String of string
+type prim_token =
+ | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *)
+ | String of string
type raw_cases_pattern_expr =
| RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t