From df954f17d5f487e06ee21e10bab1ae9a133ba72d Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Wed, 11 Jul 2012 16:42:09 +0000
Subject: Severe reorganisation of the code of tactics in Proofview.

All the purely monadic code has been moved to a new module Monads,
where, I'm afraid to confess, I got to use a number of proof transformers
to modularise the definition of tactics. It is still not easy to understand (why
would it with backtracking support?) but at least it's more robust, cleaner,
and more extensible. Plus there is now a Proofview.tclORELSE which will
be used to interprete the Ltac tactical (t1 || t2).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15596 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index a6d93aa8c5..45da00a724 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -126,6 +126,7 @@ Logic
 Refiner
 Clenv
 Evar_refiner
+Monads
 Proofview
 Proof
 Proof_global
-- 
cgit v1.2.3