aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/pbp.ml
AgeCommit message (Expand)Author
2003-03-12*** empty log message ***barras
2003-01-24Corrects the way conjunctions, existential quantifications, and arrows arebertot
2003-01-23Make proof by pointing work for the new notations of existential quantification.bertot
2003-01-22removes all references to ctast.ml the Makefile has been updated accordingly.bertot
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-12-18Integrating the Ltac language and the Blast tool into the interfacebertot
2001-11-05GROS COMMIT:barras
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-12reparationfilliatr
2001-08-10Prsingherbelin
2001-04-07Two constants had been given in the wrong package (Logic_type instead ofbertot
2001-04-04Files that handle the dialogue with the graphical user-interface pcoq.bertot