aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2001-11-12Suppression des stamps et donc des *_constraintsclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12suite du petit oupsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2185 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12petit oupsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2184 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12suite refonte extraction.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2182 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2181 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09typoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2175 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Deplacement de l'optim singleton depuis extraction vers mlutil. Autres ↵letouzey
modifs mineures git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2174 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08epsilonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2168 85f007b7-540e-0410-9357-904b9bb8a0f7
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-06Suppression des local_constraints, des ctxtty et du focus.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 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-05optimisation consistant a parfois permuter case et funletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2161 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05optim: Idset au lieu de listletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2160 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05message non barbare si extraction dans une sectionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2157 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-11-03Creation de Recursive Extarction Moduleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2152 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-02suite des modifs concernant les optimisations diversletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2151 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-01les fixpoints sont de nouveau bien optimisésletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2150 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-31suite de l'optimisation des Fixletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2149 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-31correction du debut d'optimisation du Fixletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2148 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-31multiples bricoles. Cf mon TODO papierletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2147 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-30legeres modifs pretty-print de l'extractionsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2146 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-30Reorganisation de Goption. Passage des options l'utilisant en synchroneletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2145 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-29Oups: un relicat de fn de cacheletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2143 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-25correctif bug des de Bruijn du Double Caseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2140 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-24seisme suite. correction bugsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2138 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-24Patch de goption.ml pour faire marcher les options synchrones. Passage des ↵letouzey
options d'extraction en synchrone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2137 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-23suite du seismeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2135 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-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵herbelin
sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵herbelin
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12reparationfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2110 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-01correction de deux petits bugs: case_identité trop fort et Anomaly dans le ↵letouzey
toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2091 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Correction due au changement de semantique de Matchdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2049 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20correction du eta_expanseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2028 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Report des modifs de Claudioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2024 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20bug affichage des termes ml fournisletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2022 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20utilisation du nouveau get_sort_family_ofletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2021 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-20Romegamohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19ajout du fichier CHANGESletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2004 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 01:51:22 +0000