aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacinterp.ml
Commit message (Expand)AuthorAge
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Prise en compte des noms qualifiés dans certaines commandesGravatar herbelin2000-11-20
* Ajout d'un switch pour le debuggerGravatar delahaye2000-10-30
* Bugs/Messages d'erreursGravatar herbelin2000-06-02
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Renommage command en constrGravatar herbelin2000-01-07
* modules profile, Coqinit et Coqtop (=main)Gravatar filliatr1999-12-03
* Vernacinterp et Vernacentries (partiellement)Gravatar filliatr1999-11-24