aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/minicoq.ml
Commit message (Expand)AuthorAge
* amelioration de la consommation memoire de la conversion en eta-expansantGravatar barras2001-03-23
* entetesGravatar filliatr2001-03-15
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* renommage map_constr_with_named_bindersGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* retablissement minicoq (pour Jacek)Gravatar filliatr2000-07-21
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 00:57:16 +0000