aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_proofs.ml4
Commit message (Collapse)AuthorAge
* Factorisation du '.' finalGravatar herbelin2001-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des noms longs dans les Hints et les CoercionsGravatar herbelin2001-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1272 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meta Definition + Tactic DefinitionGravatar delahaye2001-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1240 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arite cachee de Match Context + Meta DefinitionGravatar delahaye2001-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau mode de compilation de .ml4Gravatar herbelin2000-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@805 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier ↵Gravatar herbelin2000-11-05
devenu tros gros pour la compilation en PowerPC git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@800 85f007b7-540e-0410-9357-904b9bb8a0f7