diff options
| author | Pierre-Marie Pédrot | 2020-09-03 14:28:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-13 19:43:48 +0200 |
| commit | 674dcda367d9ed43f3b0cc8264a0ef10bc7fd751 (patch) | |
| tree | 9fae7950d3c560032688faf98e0aae6d2ee31c8d /tactics/class_tactics.ml | |
| parent | e1a8da8b83aa3ae96ac05c2bc6606aa0719aa64f (diff) | |
Statically ensure that only polymophic hint terms come with a context.
It is the duty of the caller to properly declare monomorphic global
constraints when creating a non-globref hint. All callers were already
abiding by this convention.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 96cbbf0ba8..b4d7e7d7f0 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -158,7 +158,7 @@ let unify_resolve ~with_evars flags h diff = match diff with | None -> Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h | Some (diff, ty) -> - let () = assert (not h.hint_poly) in + let () = assert (Option.is_empty h.hint_uctx) in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -203,11 +203,10 @@ let unify_resolve_refine flags h diff = let with_prods nprods h f = if get_typeclasses_limit_intros () then Proofview.Goal.enter begin fun gl -> - let { hint_term = c; hint_poly = poly } = h in - if poly || Int.equal nprods 0 then f None + if Option.has_some h.hint_uctx || Int.equal nprods 0 then f None else let sigma = Tacmach.New.project gl in - let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in + let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma h.hint_term in let diff = nb_prod sigma ty - nprods in if (>=) diff 0 then f (Some (diff, ty)) else Tacticals.New.tclZEROMSG (str"Not enough premisses") @@ -489,12 +488,12 @@ let make_resolve_hyp env sigma st only_classes pri decl = let hints = build_subclasses ~check:false env sigma id empty_hint_info in (List.map_append (fun (path,info,c) -> - let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in - make_resolves env sigma ~name:(PathHints path) info ~check:true ~poly:false h) + let h = IsConstr (EConstr.of_constr c, None) [@ocaml.warning "-3"] in + make_resolves env sigma ~name:(PathHints path) info ~check:true h) hints) else [] in - (hints @ make_resolves env sigma pri ~name ~check:false ~poly:false (IsGlobRef id)) + (hints @ make_resolves env sigma pri ~name ~check:false (IsGlobRef id)) else [] let make_hints g (modes,st) only_classes sign = |