aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/vtp.ml
Commit message (Expand)AuthorAge
* all tactics should be covered now: remainsGravatar bertot2003-01-26
* Add translations for many tactics but a dozen are still remainingGravatar bertot2003-01-25
* removes all references to ctast.ml the Makefile has been updated accordingly.Gravatar bertot2003-01-22
* Add a few operators in the new version of xlate.ml and make sureGravatar bertot2003-01-21
* Ajoute le bon traitement pour Ring, Locate, CommentsGravatar bertot2002-12-09
* Take notations into account: numbers and the CNotation operator.Gravatar bertot2002-12-09
* Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvellesGravatar bertot2002-12-03
* correcting the treatment of many tactics that use quant_hyp in file xlate.mlGravatar bertot2002-10-06
* Previous version did compile but did not make it possible to actually runGravatar bertot2002-10-03
* Integrating the Ltac language and the Blast tool into the interfaceGravatar bertot2001-12-18
* GROS COMMIT:Gravatar barras2001-11-05
* Adding files for the production of textual explanations as used in pcoq.Gravatar bertot2001-04-18
* Files that handle the dialogue with the graphical user-interface pcoq.Gravatar bertot2001-04-04