diff options
| author | Emilio Jesus Gallego Arias | 2020-04-18 20:22:13 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-21 08:39:12 +0200 |
| commit | 688a0869f6b8ab3048a545f821f45bc5599ba63b (patch) | |
| tree | 057e56abc232ccaeac63723f9add8f969e67393c /vernac/comHints.mli | |
| parent | c30594f55750996398eb3947838eaf1f906f08c9 (diff) | |
[hints] Move and split Hint Declaration AST to vernac
This moves the vernacular part of hints to `vernac`; in particular, it
helps removing the declaration of constants as parts of the `tactic`
folder.
Diffstat (limited to 'vernac/comHints.mli')
| -rw-r--r-- | vernac/comHints.mli | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/vernac/comHints.mli b/vernac/comHints.mli new file mode 100644 index 0000000000..77fbef5387 --- /dev/null +++ b/vernac/comHints.mli @@ -0,0 +1,29 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Typeclasses + +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + +type reference_or_constr = + | HintsReference of Libnames.qualid + | HintsConstr of Constrexpr.constr_expr + +type hints_expr = + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * Libnames.qualid list * int option + | HintsImmediate of reference_or_constr list + | HintsUnfold of Libnames.qualid list + | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool + | HintsMode of Libnames.qualid * Hints.hint_mode list + | HintsConstructors of Libnames.qualid list + | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument + +val interp_hints : poly:bool -> hints_expr -> Hints.hints_entry |