diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index c99e591fe..730da147a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -34,6 +34,7 @@ open Tacred open Printer open Vernacexpr open Sigma.Notations +open Context.Named.Declaration (****************************************) (* General functions *) @@ -727,11 +728,12 @@ let make_resolves env sigma flags pri poly ?name cr = ents (* used to add an hypothesis to the local hint database *) -let make_resolve_hyp env sigma (hname,_,htyp) = +let make_resolve_hyp env sigma decl = + let hname = get_id decl in try [make_apply_entry env sigma (true, true, false) None false ~name:(PathHints [VarRef hname]) - (mkVar hname, htyp, Univ.ContextSet.empty)] + (mkVar hname, get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp") @@ -1061,7 +1063,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = (* Not clever enough to construct dependency graph of evars *) error "Not clever enough to deal with evars dependent in other evars."; raise (Found (c,t)) - | _ -> iter_constr find_next_evar c in + | _ -> Constr.iter find_next_evar c in let rec iter c = try find_next_evar c; c with Found (evar,t) -> |