aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrexpr.ml')
-rw-r--r--interp/constrexpr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 757d186c8b..f3d0888fee 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -53,11 +53,11 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
sign flag. Note that this representation is not unique, due to possible
multiple leading zeros, and -0 = +0 *)
-type sign = bool
+type sign = SPlus | SMinus
type raw_natural_number = string
type prim_token =
- | Numeral of raw_natural_number * sign
+ | Numeral of sign * raw_natural_number
| String of string
type instance_expr = Glob_term.glob_level list