aboutsummaryrefslogtreecommitdiff
path: root/toplevel/minicoq.ml
AgeCommit message (Expand)Author
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Renommage canonique :herbelin
2000-10-01renommage map_constr_with_named_bindersherbelin
2000-09-14Abstraction de constrherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
2000-07-25retablissement make doc et make minicoqfilliatr
2000-07-21retablissement minicoq (pour Jacek)filliatr
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-03-31Portage (pour la forme) de minicoqherbelin
1999-12-03modules profile, Coqinit et Coqtop (=main)filliatr
1999-12-01mise au point Declare et avancee dans Asttermfilliatr
1999-12-01 - Typing -> Safe_typingfilliatr
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