diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-04 18:56:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-04 18:56:28 +0200 |
| commit | 6b447d6666aa44edbf69c69e9267b5031d7c7191 (patch) | |
| tree | 0bc05c98d41c3294eda2ee50f46e8bf7065a7e0d /vernac/vernacexpr.ml | |
| parent | 1136dde7b523047e6091d6e6decb45183e42fc21 (diff) | |
| parent | 852e6f960d3fc6d4cf702ab21cfe813d9edbb531 (diff) | |
Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index fb40f0d9c..9e8dfc4f8 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -124,6 +124,7 @@ type hint_info_expr = Hints.hint_info_expr type hints_expr = Hints.hints_expr = | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list + | HintsResolveIFF of bool * reference list * int option | HintsImmediate of Hints.reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool |