diff options
| author | Pierre-Marie Pédrot | 2015-10-29 19:14:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-29 19:22:59 +0100 |
| commit | 250df8586a776eaadc3553b5ceef98d3696fffdb (patch) | |
| tree | 2e86418dead74cc799f2838b43c8f602dc70cad3 /tactics/auto.ml | |
| parent | f02f64a21863ce03f2da4ff04cd003051f96801f (diff) | |
Removing the evar_map argument from s_enter.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 4a520612f8..4fb4b32632 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -119,7 +119,8 @@ let exact poly (c,clenv) = let ctx = Evd.evar_universe_context clenv.evd in ctx, c in - Proofview.Goal.s_enter { s_enter = begin fun gl sigma -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in let sigma = Sigma.to_evar_map sigma in let sigma = Evd.merge_universe_context sigma ctx in Sigma.Unsafe.of_pair (exact_check c', sigma) |