diff options
| author | Matej Kosik | 2016-02-17 11:16:27 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-02-17 11:16:27 +0100 |
| commit | 93c03652fea5914307b0a6b72b7fec6f9aaec305 (patch) | |
| tree | fe9e5e983452d5489550e9322d42067e4b213e19 /tactics/hints.ml | |
| parent | 06fa0334047a9400d0b5a144601fca35746a53b8 (diff) | |
| parent | 1dddd062f35736285eb2940382df2b53224578a7 (diff) | |
CLEANUP: Context.{Rel,Named}.Declaration.t
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 c99e591fe6..730da147af 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) -> |