From 4579e180f86923a455a5dc7edf0c1caafe583041 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 3 Feb 2017 09:02:19 +0100
Subject: reduce syntactic noise

---
 engine/proofview.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 9c264439be..1181d2bab4 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 ;
-- 
cgit v1.2.3