aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/centaur.ml4
Commit message (Expand)AuthorAge
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* removes several warnings in contrib/interfaceGravatar bertot2006-01-11
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Achèvement suppression traducteur dans contrib/interfaceGravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* adds a new command for searching a pattern inside the premises of theoremsGravatar bertot2004-02-16
* removes a lot comments that may be useful for later code maintenance, butGravatar bertot2004-02-11
* 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