diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-12 17:57:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-12 17:57:14 +0000 |
| commit | 65e08809965db4111309d9080b35be43b467f52e (patch) | |
| tree | 5cf3898c50cfdee023638c3d0c9129f580b086b4 /Coq.bat | |
| parent | f9d7ccaf40f7f21ce0630c9b668581249a635de9 (diff) | |
- Préservation des appels récursifs de tête dans ltac (réponse au "wish"
implicite du rapport de bug #468); utilisation pour cela d'un
mécanisme différent de localisation des échecs Ltac (mécanisme
probablement à affiner).
- Factorisation au passage des appels au débuggeur Ltac.
- Trivialités en passant dans clenv.ml.
- Tentative de documentation de l'infâme Reductionops.instance et essai
de déplacement plus amont du test "s = []".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10222 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Coq.bat')
0 files changed, 0 insertions, 0 deletions