diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 36a0d237d..0ba2610c4 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -108,11 +108,11 @@ type comment = | CommentInt of int type hints = - | HintsResolve of (identifier option * constr_expr) list - | HintsImmediate of (identifier option * constr_expr) list - | HintsUnfold of (identifier option * reference) list - | HintsConstructors of identifier option * reference list - | HintsExtern of identifier option * int * constr_expr * raw_tactic_expr + | HintsResolve of constr_expr list + | HintsImmediate of constr_expr list + | HintsUnfold of reference list + | HintsConstructors of reference list + | HintsExtern of int * constr_expr * raw_tactic_expr | HintsDestruct of identifier * int * (bool,unit) location * constr_expr * raw_tactic_expr |