diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-12 23:42:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-12 23:42:17 +0000 |
| commit | c33019051c716916414320b8b676202b18e2e8e4 (patch) | |
| tree | e9a175745ac58c5e34731b08a210a82d3e4d4274 /Coqide.bat | |
| parent | 34f5b0b4adce95d8eebc7f8667e841c4d4022067 (diff) | |
Suite au mail de Lionel a propos du Makefile:
1) Disparition de test_extraction.v rebasculé dans test-suite/success/extraction.v
Au passage, remplacement de quelques Set en Type pour ne pas avoir besoin du
-impredicative-set. Et ajout de passes d'extraction en Haskell et Scheme.
Simplification du Makefile en conséquence (plus de barestate)
2) Au passage, reparation (et embellissement) de extract_env. Depuis
le passage de Claudio dans cette portion (il y a 2 ans ?),
faire Extraction S (ou tout autre constructeur) echouait. Idem pour
un nom d'inductif mutuel autre que le premier du paquet. Etonnant que
personne n'ait remarqué ca plus tot...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9484 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Coqide.bat')
0 files changed, 0 insertions, 0 deletions