aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/minicoq.ml
Commit message (Expand)AuthorAge
* Portage (pour la forme) de minicoqGravatar herbelin2000-03-31
* modules profile, Coqinit et Coqtop (=main)Gravatar filliatr1999-12-03
* mise au point Declare et avancee dans AsttermGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* deplacement des var. ex. dans proofsGravatar filliatr1999-10-08
* affichage des erreurs de typage dans minicoqGravatar filliatr1999-09-10
* minicoq: pretty-print applications; ambiguite grammaire supprimee; Ind, Const...Gravatar filliatr1999-09-08
* instanciation des opérateurs sur la bonne signature (celle deGravatar filliatr1999-09-07
* - minicoq : definition inductifs; syntaxe a->bGravatar filliatr1999-09-07
* mise en place commandes minicoqGravatar filliatr1999-09-07
* (debut) de grammaire minicoqGravatar filliatr1999-09-07
* un mini toplevel pour tester le noyauGravatar filliatr1999-09-06