From 3e5de6e07bd1c86a1a6da4545039292c887d6db8 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:36:49 +0000
Subject: Various rewriting, mostly for speed purposes.

- A variant of tclEVARS directly in the language of the monad
- A variant of tclDISPATCHGEN (tclINDEPENDENT) hopefully faster in the case there is only one tactic to copy
- A better written tclDISPATCHGEN (which may make thing actually a little slower)
- A special case in tclDISPATCHGEN and tclINDEPENDENT for the case when they are 0 or 1 goals (adaptation of a patch sent by Pierre-Marie Pédrot)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16990 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 bootstrap/Monads.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'bootstrap')

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 6aae038b0a..4c800d48c6 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -1,7 +1,5 @@
 (* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)
 
-(* arnaud: on ne doit pas en avoir besoin normalement. *)
-
 Reserved Notation "'do' M x ':=' e 'in' u" (at level 200, M at level 0, x ident, e at level 200, u at level 200).
 (*Reserved Notation "'do' e ; u" (at level 200, e at level 200, u at level 200).*)
 
-- 
cgit v1.2.3