aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-11-07Biblio standard sans impredicativiteherbelin
2003-11-07majfilliatr
2003-11-06Added Instantiate ... incorbinea
2003-11-06Des oublisherbelin
2003-11-06Report des definitions sorties de fast_integer pour compatibiliteherbelin
2003-11-06majfilliatr
2003-11-05Notationsherbelin
2003-11-05Interpretation des entiers dans N (ex-entier), maj du module des positiveherbelin
2003-11-05Oubliherbelin
2003-11-05MAJherbelin
2003-11-052 espaces en tropherbelin
2003-11-05MAJherbelin
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...herbelin
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...herbelin
2003-11-05Preuve de l'incoherence de {A}+{~A} avec Set impredicatifherbelin
2003-11-05Renommage canonique d'un lemme redondantherbelin
2003-11-05Redondancesherbelin
2003-11-05Modules obsoletes de ZArith en v8herbelin
2003-11-05Nouvelle vague de renommageherbelin
2003-11-05Déport des lemmes de Omega de ZArith vers OmegaLemmasherbelin
2003-11-05Ajout NArith et restructuration ZArithherbelin
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...herbelin
2003-11-05MAJherbelin
2003-11-05Renommage canonique d'un lemme redondantherbelin
2003-11-05Branchement de Show Script sur l'afficheur structureherbelin
2003-11-05Amelioration de l'afficheur de script structureherbelin
2003-11-05majfilliatr
2003-11-04En v8, une notation, c'est 2 regles et un niveauherbelin
2003-11-04Amelioration message d'erreurherbelin
2003-11-04*** empty log message ***barras
2003-11-04Explicitation message d'erreur nombres negatifsherbelin
2003-11-04Pour eviter des anomalies au lieu d'erreur en mode traducteurherbelin
2003-11-04Extension de zarithherbelin
2003-11-04Amelioration message d'erreur pour ltacherbelin
2003-11-04Amelioration message d'erreur avec pretyping; prise en compte syntactic def d...herbelin
2003-11-04pour que make clean efface ide/utf8_convert.ml venant d'un .mllletouzey
2003-11-03Check en plus parmi les keywordsletouzey
2003-11-03Exporting ^; utilisation arg scope impliciteherbelin
2003-11-03Compatibilite V7.4 pour le delimiteur de positiveherbelin
2003-11-03majfilliatr
2003-11-02Cosmetiqueherbelin
2003-11-02Renforcement significatif du resultat principalherbelin
2003-11-02Rien de bien importantherbelin
2003-11-02Commentairesherbelin
2003-11-02MAJherbelin
2003-11-02Le printeur de Show Script n'etait pas le bon en v7herbelin
2003-11-02Typoherbelin
2003-11-02Ajout Diaconescu.vherbelin
2003-11-02AC + EXT -> EMherbelin
2003-11-02Relations entre le choix (forme relationnelle) avec restriction ou nonherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-16 16:22:20 +0000