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/hints.ml | |
| parent | ebaaa7371c3a3548ccec1836621726f6d829858a (diff) | |
Factorize code in hint declaration.
This allows to remove internal API from the mli as well.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |