Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | - documentation repertoire proofs/ | 1999-10-20 | ||
* | module Logic | 1999-10-14 | ||
* | - re-introduction d'une evar_map dans unsafe_env | 1999-10-13 | ||
* | deplacements des var. ex. hors du noyau | 1999-10-08 | ||
* | - un effort sur la doc (ocamlweb) | 1999-09-19 | ||
* | affichage des erreurs de typage dans minicoq | 1999-09-10 | ||
* | - environnements vides | 1999-09-03 | ||
* | ajout des inductifs (sans types singletons pour l'instant) | 1999-08-30 | ||
* | suppression champs inutiles dans constantes et inductifs; verification defini... | 1999-08-27 | ||
* | mach et himsg; typage sans extraction | 1999-08-24 | ||
* | - suppression de CONV_X et CONV_X_LEQ : les univers sont maintenant toujours | 1999-08-23 | ||
* | machine: execute = typage avec univers | 1999-08-20 | ||
* | mise en place programmation literaire (generation de doc/coq.tex) | 1999-08-19 | ||
* | module Reduction (debut) | 1999-08-18 | ||
* | generic, term et evd | 1999-08-17 |