diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 0499ba200e..5fb519cc4f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -878,7 +878,7 @@ let fresh_global_or_constr env sigma poly cr = else begin if isgr then warn_polymorphic_hint (pr_hint_term env sigma ctx cr); - Declare.declare_universe_context ~poly:false ctx; + DeclareUctx.declare_universe_context ~poly:false ctx; (c, Univ.ContextSet.empty) end @@ -1437,8 +1437,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.Proof.get_proof pf in - let Proof.{goals;sigma} = Proof.data pts in + let Proof.{goals;sigma} = Proof.data pf in match goals with | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> |