aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/minicoq.ml
Commit message (Expand)AuthorAge
* 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