aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/centaur.ml4
Commit message (Expand)AuthorAge
* Suppression SearchNamed finalement redondant avec SearchAboutGravatar herbelin2003-11-10
* Conjecture declare maintenant un axiome; reorganisation VernacDefinitionGravatar herbelin2003-10-23
* Integration de SearchNamed dans SearchAboutGravatar herbelin2003-10-22
* Ajout d'une fonction de recherche sur les composantes du nom des objetsGravatar herbelin2003-10-13
* show_subgoals dans PfeditGravatar herbelin2003-10-10
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* all tactics should be covered now: remainsGravatar bertot2003-01-26
* Inspect does not work for pcoq and there is no simple fix because inspectGravatar bertot2003-01-24
* Make sure proof by pointing works.Gravatar bertot2003-01-23
* removes all references to ctast.ml the Makefile has been updated accordingly.Gravatar bertot2003-01-22
* Ajout du vernac Proof withGravatar gregoire2002-12-12
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
* Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvellesGravatar bertot2002-12-03
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Previous version did compile but did not make it possible to actually runGravatar bertot2002-10-03
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...Gravatar herbelin2002-06-05
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29