diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-09 23:24:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | 2194292dbe88674fd9a606bb22f28d332f670f77 (patch) | |
| tree | 21c2e91b13a5de21856554b17f5dfaa61101e253 /tactics/hints.mli | |
| parent | af7a9a4e44739968b68aeb1cb0a1f70a1aa34e88 (diff) | |
Revise syntax of Hint Cut
As noticed by C. Cohen it was confusingly different from standard
notation.
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index df9d79212..29a4f4608 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -40,6 +40,7 @@ type raw_hint = constr * types * Univ.universe_context_set type hints_path_atom = | PathHints of global_reference list + (* For forward hints, their names is the list of projections *) | PathAny type 'a with_metadata = private { |