aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/test
AgeCommit message (Collapse)Author
2001-11-07Refonte du fichier mlutil.ml. Correction d'un bug d'optim caseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2167 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06suite des testsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2166 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05refonte du testletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2162 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-03changement epsilonesqueletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2155 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-03retablissement de l'optim case constantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2154 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-03ajout du script qualify2open qui met des open Truc en debut de fichierletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2153 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-26Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ↵letouzey
ETC etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2141 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-22chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les ↵letouzey
options git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2133 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20changements mineurs du testletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2020 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19adaptation a la nouvelle syntaxe Extract Inlined Constantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2001 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10changement du make depend en vu du make realsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1948 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-222 bugs: typevarlist pour inductifs + args pour flexiblesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1800 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-14mise en place extraction haskellfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1751 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-09nettoyage extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1737 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25make reals prend en compte tous les .vo de theories/Realsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1712 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24TODO in v.o., test/Makefile moins pire, README avec refletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1694 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Ajout du .dependmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1693 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Retire theories/Nummohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1692 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Fin d'optimisation (cas modules) + warning pour coind & ocamlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1685 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23mise a jourletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1671 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23realisation des realsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1670 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Remaniement Makefile de test. make reals possibleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1661 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19scripts; extraction False_recfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1635 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19blindage False_recfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19modifs des scripts de test autofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1621 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19script de bench automatique pour extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1615 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-13eliminiation des singletons du genre sig + diversletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1587 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30repertoire pour les tests d'extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1504 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-14 18:08:16 +0000