aboutsummaryrefslogtreecommitdiff
path: root/library/global.ml
AgeCommit message (Expand)Author
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2000-11-26Calcul du chemin optimal dans qualid_of_globalherbelin
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon S...filliatr
2000-11-23Fonction qualid_of_global pour affichage des paths avec des '.'herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Renommage canonique :herbelin
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-05-31Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
1999-12-05add_leaf -> application methode cachefilliatr
1999-12-01 - environment -> safe_environmentfilliatr
1999-12-01 - Typing -> Safe_typingfilliatr
1999-11-26Evd vient apres Environ -> id_of_existential expansefilliatr
1999-11-26ajouts divers pour module Printerfilliatr
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
1999-11-22modules Indrec, Wcclausenv; progression dans Tacticalsfilliatr
1999-10-22 - module Redinfo dans library/ pour les constantes d'éliminationfilliatr
1999-10-08deplacement des var. ex. dans proofsfilliatr
1999-09-27ajout des constraintes pendant le chargement d'un module (load)filliatr
1999-09-19 - un effort sur la doc (ocamlweb)filliatr
1999-09-18module Libraryfilliatr
1999-09-09environement globalfilliatr