aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_proofs.ml4
Commit message (Expand)AuthorAge
* Factorisation du '.' finalGravatar herbelin2001-01-27
* Prise en compte des noms longs dans les Hints et les CoercionsGravatar herbelin2001-01-24
* Meta Definition + Tactic DefinitionGravatar delahaye2001-01-09
* Arite cachee de Match Context + Meta DefinitionGravatar delahaye2001-01-05
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* Nouveau mode de compilation de .ml4Gravatar herbelin2000-11-05
* Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...Gravatar herbelin2000-11-05