aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-11-17User Casts are for helping pretyping, experimentally not to be keptherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2198 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2197 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-16*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2196 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-15Ajout d'un fichier Max dans Arith, et enrichissement du Min.letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2195 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-15Ajout des fonctions tail-recursives tail_plus et tail_mult.letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2194 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-14Une liste plus precise des .v a prendre en compte pour les dependances, a ↵herbelin
l'exclusion notamment des .v de la suite de tests git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2193 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-14oubli: changement de nil en nilTmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2192 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-14Changement de list en listT, cons en consT et app en appTmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2191 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-14Suppression d'Export redondantsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2190 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-14Revolution culturelle: suppression des arguments propletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2189 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-13Moins de fichiers avec des axiomsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2188 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12suppression d'axiomes dans Rstar, Newman et Integersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2187 85f007b7-540e-0410-9357-904b9bb8a0f7
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-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 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-09MAJ après restructuration kernelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2180 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09Nettoyage coercions et classesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2179 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09Déplacement et export de type_of_global dans Globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2178 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09MAJ pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2177 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2176 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-08Quelques tests sur le let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2173 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Introduction d'univers frais dans les types implicites engendrés par le ↵herbelin
prétypage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2172 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Rétablissement de la persistance des Cast; typage des LetIn sans recours à ↵herbelin
Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2171 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]bherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2170 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Choucroute entre les tables de synchronisation, les options -silent et les ↵letouzey
etats initiaux de coq. Pour l'instant je remets Silent en asynchrone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2169 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-06corrections mineures suite au commit de restructuration du noyaubarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06Suite de la suppression : enamed_declaration est remplace par evar_map.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2164 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-05Oopsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2159 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-03interversion de deux Elim dans In_dec pour que la fonction extraite soit ↵letouzey
efficace git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2156 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 12:28:23 +0000