diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 6250886821..6d623f1c34 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -33,6 +33,7 @@ open Pfedit open Tacred open Printer open Vernacexpr +open Sigma.Notations (****************************************) (* General functions *) @@ -1184,6 +1185,12 @@ let add_hint_lemmas env sigma eapply lems hint_db = Hint_db.add_list env sigma hintlist' hint_db let make_local_hint_db env sigma ts eapply lems = + let map c = + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (c, sigma, _) = c.delayed env sigma in + (Sigma.to_evar_map sigma, c) + in + let lems = List.map map lems in let sign = Environ.named_context env in let ts = match ts with | None -> Hint_db.transparent_state (searchtable_map "core") |