diff options
| author | Emilio Jesus Gallego Arias | 2020-04-11 17:14:38 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-15 11:12:53 -0400 |
| commit | 1dc70876b4a5ad027b3b73aa6ba741e89320d17d (patch) | |
| tree | 13a69ee4c6d0bf42219fef0f090195c3082449f4 /tactics/hints.ml | |
| parent | e262a6262ebb6c3010cb58e96839b0e3d66e09ac (diff) | |
[declare] Rename `Declare.t` to `Declare.Proof.t`
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index a2edafb376..ffb0e030db 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1562,7 +1562,7 @@ let pr_hint_term env sigma cl = (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint pf = let env = Global.env () in - let pts = Declare.get_proof pf in + let pts = Declare.Proof.get_proof pf in let Proof.{goals;sigma} = Proof.data pts in match goals with | [] -> CErrors.user_err Pp.(str "No focused goal.") |