aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
AgeCommit message (Expand)Author
2009-01-10- Fixed the recompilation of config/revision.ml once every two conmpilations.herbelin
2009-01-08Minor doc fixes:msozeau
2009-01-07Suite de la révision #11756notin
2009-01-06Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...notin
2009-01-06Report de la révision 11754 (compilation sous windows)notin
2009-01-04Moved JProver to a user contribution (as was decided a long time ago)herbelin
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
2008-12-16Take advantage of natdynlink when available: almost all contribs become loada...letouzey
2008-12-16Move FunctionalExtensionality to Logic/ (someone please check that themsozeau
2008-11-12Correction du bug #1995notin
2008-10-28Native "Declare ML Module" when possibleglondu
2008-10-18- Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)herbelin
2008-09-07Do not install csdpcert in $(BINDIR)glondu
2008-09-06Install coqide manpageglondu
2008-09-06More cleaningglondu
2008-09-06Use $(COQTOPEXE) to refer to bin/coqtop in Makefilesglondu
2008-09-05Build coqrun library using ocamlmklib...glondu
2008-09-02Initial implementation of a new command to define (dependent) functions bymsozeau
2008-09-02added Makefile target: validate (to recheck all .vo in a row)barras
2008-08-18Renaming parser -> coq-parserglondu
2008-08-16Install csdpcert with librariesglondu
2008-08-07micromega : bug fixes and optimisationsfbesson
2008-08-04Évolutions diverses et variées.herbelin
2008-07-27Now, -browser option is effective (and compiles)glondu
2008-07-17- Suppression de Rstar/Newman peu utilisables comme biblio (encodageherbelin
2008-07-16Ajout de cibles pour le manuel de référence (refman-nodep, stdlib-nodep, re...notin
2008-07-07Micromega: doc + test-suite updatefbesson
2008-06-25Some work on BigQ :letouzey
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-25Report de la révision #11175 de la branche v8.2 vers le trunknotin
2008-06-25Micromega : bugs fixes - renaming of tactics - documentationfbesson
2008-06-24Suppression de l'option -dump-glob et ajout d'une option -no-globnotin
2008-06-12Remplacement des 'cp' et 'mkdir' par 'install'notin
2008-06-062-3 petites modifs pour la compilation sous Windows...notin
2008-06-03Fix setoid_rewrite documentation examples.msozeau
2008-06-03In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
2008-06-01Quelques amendements liées à la compilation des packages.herbelin
2008-06-01BigQ: starting to create and use an interface QSigletouzey
2008-06-01Enhance the BigN and BigZ infrastructure: letouzey
2008-05-29NBigN: proofs that BigN implements axioms of NAxiomsSigletouzey
2008-05-27Cyclic31 : proof of the spec of gcd31letouzey
2008-05-22Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...letouzey
2008-05-22QRewrite is now obsolete. It was containing manual ltac stuffletouzey
2008-05-22added coqchk to the main Makefile and a make variable VALIDATE to check the v...barras
2008-05-19Intégration de micromega ("omicron" pour fourier et sa variante sur Z,herbelin
2008-05-17ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsletouzey
2008-05-16Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurateletouzey
2008-05-16BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZletouzey
2008-05-16ZTreeMod was meant to prove that BigZ correspond to the Integer Axioms.letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:02:48 +0000