diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 22430b7ed..16589805f 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -286,7 +286,7 @@ type vernac_expr = (* Commands *) | VernacDeclareTacticDefinition of - rec_flag * (lident * bool * raw_tactic_expr) list + rec_flag * (reference * bool * raw_tactic_expr) list | VernacHints of locality_flag * lstring list * hints | VernacSyntacticDefinition of identifier * (identifier list * constr_expr) * locality_flag * onlyparsing_flag |