diff options
author | 2014-02-27 15:29:03 +0100 | |
---|---|---|
committer | 2014-02-27 15:29:03 +0100 | |
commit | edd06dfa60a3535b93da92bdc0f26e412c3e2d6c (patch) | |
tree | 8fce7f1e6c074db8187f6e13ecbfde438df29568 /tactics/tacinterp.ml | |
parent | 0dfc87c68d5aba5adac079cb62ae504d82b303b9 (diff) |
Tacinterp: more refactoring.
Introducing List.fold_right and List.fold_left in Monad.
Diffstat (limited to 'tactics/tacinterp.ml')
-rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 7d9720614..ca2c91485 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; |