aboutsummaryrefslogtreecommitdiff
path: root/.depend.camlp4
AgeCommit message (Expand)Author
2005-03-16tactiques prouveurs premier ordre dans contrib/dp/coq
2005-02-04Ajout g_xml.ml4 et cic2Xml.mlherbelin
2004-08-26majfilliatr
2004-07-29majfilliatr
2004-07-16MAJherbelin
2004-05-04majfilliatr
2004-01-28majfilliatr
2004-01-15majfilliatr
2003-10-16Ground update + Linear removalcorbinea
2003-07-02suppression de newtautocorbinea
2003-06-15Ground major update ... mmm, sounds exciting !corbinea
2003-05-26moved engine.ml4 to ground.ml4, added option 'Ground Depth'corbinea
2003-04-25Added the Ground tactic.corbinea
2003-03-12* Ajout du traducteur nouvelle syntaxe *barras
2003-02-28majfilliatr
2003-02-27The contribution of Pierre Courtieu on generating specialized induction schemesbertot
2003-02-24Bringing Linear back to life (Still somewhat buggy).corbinea
2003-01-23Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).corbinea
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-10-01Adding the congruence closure tactics (CC and CCsolve).corbinea
2002-09-20majfilliatr
2002-09-20majfilliatr
2002-08-02Modules dans COQ\!\!\!\!coq
2002-06-07extraction vers schemeletouzey
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-12-19contrib/interface/dad.ml4 had no real need of streams, it should have beenbertot
2001-12-19reparation du make depend et du .dependletouzey
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...herbelin
2001-04-19Ajout de Fielddelahaye
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
2001-04-08Ajout lemmes arithmetiquesmohring
2001-03-30branchement extraction (bytecode seulement)filliatr
2001-02-08simplification du make depend; fonctions de stat. util. memoire dans certains...filliatr
2001-02-05calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)filliatr
2000-11-29mise a jourfilliatr
2000-11-05MAJherbelin
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
2000-10-31- simplification Makefile (compilation des fichiers .ml'; pas encore parfaitfilliatr
2000-09-18mise a jour dependancesfilliatr
2000-09-10Suppression de Abstherbelin
2000-03-08MAJherbelin
2000-01-07Renommage command en constrherbelin
1999-12-05premier debugagefilliatr
1999-12-03 - global_reference traite des variablesfilliatr
1999-10-20modules Evar_refiner et Typing_evfilliatr