diff options
| author | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
| commit | e5581b2a1e5b3d9fc5dc7fe95ee4ba121f5d42cd (patch) | |
| tree | 1a0d0b7d693c37ca8712057e946587584687208e /tactics/hints.ml | |
| parent | 2f23c27e08f66402b8fba4745681becd402f4c5c (diff) | |
| parent | 0ce9cef0ac431e184c870617841bedc3f427396d (diff) | |
Merge PR#623: Remove the Sigma (monotonous state) API.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 70e62eabac..773abb9f0c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -22,7 +22,6 @@ open Namegen open Libnames open Smartlocate open Misctypes -open Tactypes open Termops open Inductiveops open Typing @@ -34,7 +33,6 @@ open Pfedit open Tacred open Printer open Vernacexpr -open Sigma.Notations module NamedDecl = Context.Named.Declaration @@ -1363,11 +1361,7 @@ 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 map c = c env sigma in let lems = List.map map lems in let sign = EConstr.named_context env in let ts = match ts with |