Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin | 2003-05-19 |
| | | | | | | | | | Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
* | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin | 2003-04-07 |
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7 |