From 2194292dbe88674fd9a606bb22f28d332f670f77 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Jun 2016 23:24:57 +0200 Subject: Revise syntax of Hint Cut As noticed by C. Cohen it was confusingly different from standard notation. --- tactics/hints.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'tactics/hints.mli') 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 { -- cgit v1.2.3