aboutsummaryrefslogtreecommitdiff
path: root/library/global.ml
AgeCommit message (Expand)Author
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