diff options
| -rw-r--r-- | tactics/class_tactics.ml | 14 | ||||
| -rw-r--r-- | tactics/hints.ml | 8 | ||||
| -rw-r--r-- | tactics/hints.mli | 32 |
3 files changed, 10 insertions, 44 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 80c76bee60..195073d7aa 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -516,25 +516,21 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let is_class = iscl env cty in let keep = not only_classes || is_class in if keep then - let c = mkVar id in - let name = PathHints [GlobRef.VarRef id] in + let id = GlobRef.VarRef id in + let name = PathHints [id] in let hints = if is_class then - let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in + 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) - (true,false,not !Flags.quiet) info ~poly:false + (true,false,not !Flags.quiet) info ~check:true ~poly:false h) hints) else [] in - (hints @ List.map_filter - (fun f -> try Some (f (c, cty, Univ.ContextSet.empty)) - with Failure _ | UserError _ -> None) - [make_exact_entry ~name env sigma pri ~poly:false; - make_apply_entry ~name env sigma flags pri ~poly:false]) + (hints @ make_resolves env sigma flags pri ~name ~check:false ~poly:false (IsGlobRef id)) else [] let make_hints g (modes,st) only_classes sign = diff --git a/tactics/hints.ml b/tactics/hints.ml index a0670ef70d..0c23532e12 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -882,7 +882,7 @@ let fresh_global_or_constr env sigma poly cr = (c, Univ.ContextSet.empty) end -let make_resolves env sigma flags info ~poly ?name cr = +let make_resolves env sigma flags info ~check ~poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in let cty = Retyping.get_type_of env sigma c in let try_apply f = @@ -891,7 +891,7 @@ let make_resolves env sigma flags info ~poly ?name cr = [make_exact_entry env sigma info ~poly ?name; make_apply_entry env sigma flags info ~poly ?name] in - if List.is_empty ents then + if check && List.is_empty ents then user_err ~hdr:"Hint" (pr_leconstr_env env sigma c ++ spc() ++ (if pi1 flags then str"cannot be used as a hint." @@ -1183,7 +1183,7 @@ let add_resolves env sigma clist ~local ~superglobal dbnames = let r = List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> make_resolves env sigma (true,hnf,not !Flags.quiet) - pri ~poly ~name:path gr) clist) + pri ~check:true ~poly ~name:path gr) clist) in let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in Lib.add_anonymous_leaf (inAutoHint hint)) @@ -1334,7 +1334,7 @@ let expand_constructor_hints env sigma lems = let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) empty_hint_info ~poly lem) lems + make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in diff --git a/tactics/hints.mli b/tactics/hints.mli index f5fd3348e4..6c8b7fed75 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -206,36 +206,6 @@ val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_ val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t) -(** [make_exact_entry info (c, ctyp, ctx)]. - [c] is the term given as an exact proof to solve the goal; - [ctyp] is the type of [c]. - [ctx] is its (refreshable) universe context. - In info: - [hint_priority] is the hint's desired priority, it is 0 if unspecified - [hint_pattern] is the hint's desired pattern, it is inferred if not specified -*) - -val make_exact_entry : env -> evar_map -> hint_info -> poly:bool -> ?name:hints_path_atom -> - (constr * types * Univ.ContextSet.t) -> hint_entry - -(** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))]. - [eapply] is true if this hint will be used only with EApply; - [hnf] should be true if we should expand the head of cty before searching for - products; - [c] is the term given as an exact proof to solve the goal; - [cty] is the type of [c]. - [ctx] is its (refreshable) universe context. - In info: - [hint_priority] is the hint's desired priority, it is computed as the number of products in [cty] - if unspecified - [hint_pattern] is the hint's desired pattern, it is inferred from the conclusion of [cty] - if not specified -*) - -val make_apply_entry : - env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom -> - (constr * types * Univ.ContextSet.t) -> hint_entry - (** A constr which is Hint'ed will be: - (1) used as an Exact, if it does not start with a product - (2) used as an Apply, if its HNF starts with a product, and @@ -244,7 +214,7 @@ val make_apply_entry : has missing arguments. *) val make_resolves : - env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom -> + env -> evar_map -> bool * bool * bool -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom -> hint_term -> hint_entry list (** [make_resolve_hyp hname htyp]. |