diff options
| author | Pierre-Marie Pédrot | 2020-03-12 10:23:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-16 16:02:24 +0200 |
| commit | 0d3e83ad7e6dd6b1fd4863b03599defe22a45846 (patch) | |
| tree | 96808ab5335276bcc8ee1d2192edf8c041363ef4 /tactics/class_tactics.ml | |
| parent | ebaaa7371c3a3548ccec1836621726f6d829858a (diff) | |
Factorize code in hint declaration.
This allows to remove internal API from the mli as well.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 14 |
1 files changed, 5 insertions, 9 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 = |