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 /kernel/type_errors.mli | |
| 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 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions