diff options
| author | Pierre-Marie Pédrot | 2020-06-08 12:54:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | f66bd46c551915267a88d1ee2534ba091292882e (patch) | |
| tree | e42293e9c8bdc1fc2aa6888eaddd8c22a2642c0c | |
| parent | ca6dd2805b4a00cf8425337ec1d89327c94ef397 (diff) | |
Do not export flags in Hints.make_resolves.
They are always the same.
| -rw-r--r-- | tactics/class_tactics.ml | 6 | ||||
| -rw-r--r-- | tactics/hints.ml | 3 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 |
3 files changed, 6 insertions, 5 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 68a78f52f9..18994d0242 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -524,13 +524,11 @@ let make_resolve_hyp env sigma st only_classes pri decl = (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, false) info ~check:true ~poly:false - h) + make_resolves env sigma ~name:(PathHints path) info ~check:true ~poly:false h) hints) else [] in - (hints @ make_resolves env sigma (true, false, false) pri ~name ~check:false ~poly:false (IsGlobRef id)) + (hints @ make_resolves env sigma 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 0c23532e12..58fbf2fd66 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1336,6 +1336,9 @@ let constructor_hints env sigma eapply lems = List.map_append (fun (poly, lem) -> make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems +let make_resolves env sigma info ~check ~poly ?name hint = + make_resolves env sigma (true, false, false) info ~check ~poly ?name hint + let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in let lems = List.map map lems in diff --git a/tactics/hints.mli b/tactics/hints.mli index 6c8b7fed75..ecbde091cd 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -214,7 +214,7 @@ val prepare_hint : bool (* Check no remaining evars *) -> has missing arguments. *) val make_resolves : - env -> evar_map -> bool * bool * bool -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom -> + env -> evar_map -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom -> hint_term -> hint_entry list (** [make_resolve_hyp hname htyp]. |