aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.camlp4
Commit message (Expand)AuthorAge
* 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
* calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)Gravatar filliatr2001-02-05
* mise a jourGravatar filliatr2000-11-29
* MAJGravatar herbelin2000-11-05
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
* - simplification Makefile (compilation des fichiers .ml'; pas encore parfaitGravatar filliatr2000-10-31
* mise a jour dependancesGravatar filliatr2000-09-18
* Suppression de AbstGravatar herbelin2000-09-10
* MAJGravatar herbelin2000-03-08
* Renommage command en constrGravatar herbelin2000-01-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 17:34:57 +0000