aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.mli
Commit message (Expand)AuthorAge
...
* 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