From edd06dfa60a3535b93da92bdc0f26e412c3e2d6c Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 27 Feb 2014 15:29:03 +0100
Subject: Tacinterp: more refactoring.

Introducing List.fold_right and List.fold_left in Monad.---
 tactics/tacinterp.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7d9720614e..ca2c914853 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1201,12 +1201,11 @@ and interp_letrec ist llc u gl =
 
 (* Interprets the clauses of a LetIn *)
 and interp_letin ist llc u gl =
-  let fold ((_, id), body) acc =
+  let fold acc ((_, id), body) =
     interp_tacarg ist body gl >>= fun v ->
-    acc >>= fun acc ->
     Proofview.tclUNIT (Id.Map.add id v acc)
   in
-  List.fold_right fold llc (Proofview.tclUNIT ist.lfun) >>= fun lfun ->
+  Proofview.Monad.List.fold_left fold ist.lfun llc >>= fun lfun ->
   let ist = { ist with lfun } in
   val_interp ist u gl
 
@@ -2033,11 +2032,10 @@ and interp_atomic ist tac =
       in
       Proofview.Goal.enter begin fun gl ->
         let addvar (x, v) accu =
-          accu >>= fun accu ->
           f v gl >>= fun v ->
           Proofview.tclUNIT (Id.Map.add x v accu)
         in
-        List.fold_right addvar l (Proofview.tclUNIT ist.lfun) >>= fun lfun ->
+        Proofview.Monad.List.fold_right addvar l ist.lfun >>= fun lfun ->
           let trace = push_trace (loc,LtacNotationCall s) ist in
           let ist = {
             lfun = lfun;
-- 
cgit v1.2.3