aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.camlp4
Commit message (Expand)AuthorAge
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deGravatar herbelin2006-03-22
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* Julien:Gravatar bertot2006-02-08
* New version of functional induction / inversion. By Julien Forest,Gravatar coq2006-02-01
* majGravatar coq2005-12-30
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* majGravatar coq2005-11-18
* Modifications in the .depend files for the contrib/recdef directoryGravatar bertot2005-11-07
* new congruenceGravatar corbinea2005-08-17
* Subtac: traitement correct des existentielles et de la récursion.Gravatar coq2005-07-15
* reflexive tautoGravatar corbinea2005-07-15
* Added subtac contrib.Gravatar coq2005-05-25
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20
* tactiques prouveurs premier ordre dans contrib/dp/Gravatar coq2005-03-16
* Ajout g_xml.ml4 et cic2Xml.mlGravatar herbelin2005-02-04
* majGravatar filliatr2004-08-26
* majGravatar filliatr2004-07-29
* MAJGravatar herbelin2004-07-16
* majGravatar filliatr2004-05-04
* majGravatar filliatr2004-01-28
* majGravatar filliatr2004-01-15
* Ground update + Linear removalGravatar corbinea2003-10-16
* suppression de newtautoGravatar corbinea2003-07-02
* Ground major update ... mmm, sounds exciting !Gravatar corbinea2003-06-15
* moved engine.ml4 to ground.ml4, added option 'Ground Depth'Gravatar corbinea2003-05-26
* Added the Ground tactic.Gravatar corbinea2003-04-25
* * Ajout du traducteur nouvelle syntaxe *Gravatar barras2003-03-12
* majGravatar filliatr2003-02-28
* The contribution of Pierre Courtieu on generating specialized induction schemesGravatar bertot2003-02-27
* Bringing Linear back to life (Still somewhat buggy).Gravatar corbinea2003-02-24
* Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).Gravatar corbinea2003-01-23
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Adding the congruence closure tactics (CC and CCsolve).Gravatar corbinea2002-10-01
* majGravatar filliatr2002-09-20
* majGravatar filliatr2002-09-20
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* extraction vers schemeGravatar letouzey2002-06-07
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* contrib/interface/dad.ml4 had no real need of streams, it should have beenGravatar bertot2001-12-19
* reparation du make depend et du .dependGravatar letouzey2001-12-19
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...Gravatar herbelin2001-06-25
* Ajout de FieldGravatar delahaye2001-04-19
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08