diff options
Diffstat (limited to 'vernac/egramcoq.ml')
| -rw-r--r-- | vernac/egramcoq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index e7a308dda..434e836d8 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -228,7 +228,7 @@ type _ target = type prod_info = production_level * production_position type (_, _) entry = -| TTName : ('self, Misctypes.lname) entry +| TTName : ('self, lname) entry | TTReference : ('self, reference) entry | TTBigint : ('self, Constrexpr.raw_natural_number) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry |