diff options
| author | aspiwack | 2013-11-02 15:36:49 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:36:49 +0000 |
| commit | 3e5de6e07bd1c86a1a6da4545039292c887d6db8 (patch) | |
| tree | 417616c80d0cc247f52d305af938cc9ce444956e /bootstrap | |
| parent | 3abbdc46b85fdb7d8de25e727e80e57a2d4e8904 (diff) | |
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
Diffstat (limited to 'bootstrap')
| -rw-r--r-- | bootstrap/Monads.v | 2 |
1 files changed, 0 insertions, 2 deletions
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).*) |