aboutsummaryrefslogtreecommitdiff
path: root/toplevel/minicoq.ml
AgeCommit message (Expand)Author
1999-10-08deplacement des var. ex. dans proofsfilliatr
1999-09-10affichage des erreurs de typage dans minicoqfilliatr
1999-09-08minicoq: pretty-print applications; ambiguite grammaire supprimee; Ind, Const...filliatr
1999-09-07instanciation des opérateurs sur la bonne signature (celle defilliatr
1999-09-07 - minicoq : definition inductifs; syntaxe a->bfilliatr
1999-09-07mise en place commandes minicoqfilliatr
1999-09-07(debut) de grammaire minicoqfilliatr
1999-09-06un mini toplevel pour tester le noyaufilliatr