diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index ac3b3964ab..3b9bf9a55f 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -302,6 +302,7 @@ type vernac_expr = | VernacDeclareTacticDefinition of (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list) | VernacCreateHintDb of locality_flag * string * bool + | VernacRemoveHints of locality_flag * string list * reference list | VernacHints of locality_flag * string list * hints_expr | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * locality_flag * onlyparsing_flag |