From 99cfd0d1fd205f5d5ca536b2bb5414bc43ffc243 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sat, 9 Nov 2013 00:04:51 +0000
Subject: Partial applications in Goal.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17074 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/goal.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/proofs/goal.ml b/proofs/goal.ml
index a036f728d5..cd43b3202d 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -138,8 +138,8 @@ let eval t env defs gl =
 (* monadic bind on sensitive expressions *)
 let bind e f = (); fun env rdefs goal info ->
   let a = e env rdefs goal info in
-  let b = f a env rdefs goal info in
-  b
+  let r = f a in
+  r env rdefs goal info
 
 (* monadic return on sensitive expressions *)
 let return v = () ; fun _ _ _ _ -> v
@@ -169,11 +169,13 @@ module Refinable = struct
 
   let make t = (); fun env rdefs gl info ->
     let r = ref [] in
-    let me = t r env rdefs gl info in
+    let me = t r in
+    let me = me env rdefs gl info in
     { me = me; my_evars = !r }
   let make_with t = (); fun env rdefs gl info ->
     let r = ref [] in
-    let (me,side) = t r env rdefs gl info in
+    let t = t r in
+    let (me,side) = t env rdefs gl info in
     ({ me = me ; my_evars = !r }, side)
 
   let mkEvar handle env typ = (); fun _ rdefs _ _ ->
-- 
cgit v1.2.3