Merge PR#552: Miscelaneous commits

1 files changed, 6 insertions, 6 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 9c264439be..f054038e9c 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1020,11 +1020,11 @@ module Goal = struct
 
   let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t)
 
-  let env { env=env } = env
-  let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma
-  let hyps { env=env } = EConstr.named_context env
-  let concl { concl=concl } = concl
-  let extra { sigma=sigma; self=self } = goal_extra sigma self
+  let env {env} = env
+  let sigma {sigma} = Sigma.Unsafe.of_evar_map sigma
+  let hyps {env} = EConstr.named_context env
+  let concl {concl} = concl
+  let extra {sigma; self} = goal_extra sigma self
 
   let gmake_with info env sigma goal = 
     { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
@@ -1040,7 +1040,7 @@ module Goal = struct
   let nf_enter f =
     InfoL.tag (Info.Dispatch) begin
     iter_goal begin fun goal ->
-      Env.get >>= fun env ->
+      tclENV >>= fun env ->
       tclEVARMAP >>= fun sigma ->
       try
         let (gl, sigma) = nf_gmake env sigma goal in