diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 0df1a35c62..48b4505327 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1135,7 +1135,8 @@ let add_hints local dbnames0 h = if String.List.mem "nocore" dbnames0 then error "The hint database \"nocore\" is meant to stay empty."; let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in match h with | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames |