aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Expand)AuthorAge
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* adding the directives to compile the parser that is used in the graphicalGravatar bertot2001-04-04
* add the compilation of the files needed for the interface with pcoq.Gravatar bertot2001-04-04
* installation des .cmo pour l'extractionGravatar filliatr2001-04-03
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
* fichiers extractionGravatar filliatr2001-03-29
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Commentaires. Verification des assert false. Probleme des types ML arity.Gravatar letouzey2001-03-12
* modifs pour extraction; bug coqmktopGravatar filliatr2001-03-06
* module Explore générique et réécriture EAuto avec ce module; occur check ...Gravatar filliatr2001-03-05
* Inversion termast/astterm; suppression camldebug pour coqmktop -optGravatar herbelin2001-03-01
* nouvelle implantation de la reductionGravatar barras2001-03-01
* bug Reset et SectionsGravatar filliatr2001-02-28
* mise a jourGravatar filliatr2001-02-26
* Stdlib -> Coqlib, Stock disparaitGravatar herbelin2001-02-14
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirGravatar herbelin2001-02-07
* mise en place extractionGravatar filliatr2001-02-06
* EqDecideGravatar filliatr2001-02-06
* calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)Gravatar filliatr2001-02-05
* Les Objdef introduisent une convertibilité avec les projections dans le test...Gravatar herbelin2001-01-30
* backtrack sur le lexeur de la V6Gravatar filliatr2001-01-30
* Nouveau module pour centraliser les chemins des constantes globales utilisée...Gravatar herbelin2001-01-19
* Pattern sera mieux dans Pretyping; relâchement head_pattern_boundGravatar herbelin2000-12-26
* Insertion COQPATHPREFIX pour isntallation localeGravatar herbelin2000-12-22
* tests automatiquesGravatar herbelin2000-12-09
* Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...Gravatar herbelin2000-12-06
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Changement de la syntaxe des options -I et -RGravatar herbelin2000-11-30
* Ajout d'une option d'alias à -IGravatar herbelin2000-11-29
* Added -R inclusion to fix compilation in not-local configuration.Gravatar sacerdot2000-11-28
* -I inutiles pour coqc et utilisation de -R theories (pour garder trace des no...Gravatar herbelin2000-11-28
* Rajout de PolyListSyntax aussi dans MakefileGravatar herbelin2000-11-28
* Xml contrib retachedGravatar sacerdot2000-11-27
* Ajout BEST partout a coqcGravatar filliatr2000-11-24
* SearchPattern et SearchRewriteGravatar filliatr2000-11-24
* Ajout d'une syntaxe pour Reals.Gravatar mayero2000-11-23
* retablissement de line_oriented_parser pour YvesGravatar filliatr2000-11-22
* des proofs/macros qui trainaient dans le Makefile et le .dependGravatar filliatr2000-11-22
* Ajout du clean pour tolink.mlGravatar delahaye2000-11-21
* ln -sf au lieu de ln -sGravatar filliatr2000-11-21
* implicites manuelsGravatar filliatr2000-11-21
* ajout de theories/WellfoundedGravatar filliatr2000-11-21
* XML débranchéGravatar filliatr2000-11-21
* Prise en compte camlp4.opt dans la configuration et le MakefileGravatar herbelin2000-11-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 02:47:12 +0000