aboutsummaryrefslogtreecommitdiff
path: root/vernac/egramcoq.ml
diff options
context:
space:
mode:
authorPierre Roux2018-10-20 15:10:54 +0200
committerPierre Roux2019-04-02 00:02:16 +0200
commit4dc3d04d0812005f221e88744c587de8ef0f38ee (patch)
tree3d66f0198cc168403ec27fd04ac310a0b5c56b1d /vernac/egramcoq.ml
parenta95aacce6cc32726b494d4cc694da49eae86cf96 (diff)
Rename raw_natural_number to raw_numeral
In anticipation of an extension from natural numbers to other numeral constants.
Diffstat (limited to 'vernac/egramcoq.ml')
-rw-r--r--vernac/egramcoq.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index b913bccfa3..01e59bbed6 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -245,7 +245,7 @@ type prod_info = production_level * production_position
type (_, _) entry =
| TTName : ('self, lname) entry
| TTReference : ('self, qualid) entry
-| TTBigint : ('self, Constrexpr.raw_natural_number) entry
+| TTBigint : ('self, Constrexpr.raw_numeral) entry
| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry