diff options
| author | Matej Košík | 2017-04-10 16:03:36 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-04-10 16:03:36 +0200 |
| commit | e248b3d45835695c3bcf7c60e80172919025cd64 (patch) | |
| tree | 358fe7676d86b3d1fbe0980612640295b390eabc /engine | |
| parent | c6f7619e1d8c2971041610f31b4be3e468f68593 (diff) | |
Revert "trivial"
This reverts commit 9b627431516f2cf88312329def9e0ec5e8605a98.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 60862d4216..acd931160f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1042,7 +1042,7 @@ module Goal = struct let nf_enter f = InfoL.tag (Info.Dispatch) begin iter_goal begin fun goal -> - tclENV >>= fun env -> + Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in |