aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.mli
Commit message (Expand)AuthorAge
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* module WcclausenvGravatar filliatr1999-11-22
* - module Redinfo dans library/ pour les constantes d'éliminationGravatar filliatr1999-10-22
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* module LogicGravatar filliatr1999-10-14
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
* ensembles de contraintes d'universGravatar filliatr1999-09-25
* ajout des inductifs (sans types singletons pour l'instant)Gravatar filliatr1999-08-30
* un petit effort de presentation dans les interfacesGravatar filliatr1999-08-30
* suppression champs inutiles dans constantes et inductifs; verification defini...Gravatar filliatr1999-08-27
* modules Instantiate, Constant et InductiveGravatar filliatr1999-08-25
* mach et himsg; typage sans extractionGravatar filliatr1999-08-24
* - suppression de CONV_X et CONV_X_LEQ : les univers sont maintenant toujoursGravatar filliatr1999-08-23
* machine: execute = typage avec universGravatar filliatr1999-08-20
* mise en place programmation literaire (generation de doc/coq.tex)Gravatar filliatr1999-08-19
* module Reduction (fin)Gravatar filliatr1999-08-18
* module Reduction (debut)Gravatar filliatr1999-08-18