aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
AgeCommit message (Expand)Author
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
2008-05-16More BigNum cleanup: letouzey
2008-05-15Oubli lors de la révision 10899 (Bool_nat.vo)notin
2008-05-09Still Ints-->Numbers transition: fix the previous commit about a typoletouzey
2008-05-08Still Ints-->Numbers transition: fix a typo preventing the compilation of BigQletouzey
2008-05-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey
2008-04-28menage dans funind + deplaceemnt de recdef dans funindjforest
2008-04-27Suite r10857herbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-21Addded the "Dump Tree" command.cek
2008-04-17tactique gappafilliatr
2008-04-17Add almost empty Classes.tex for documentation of type classes.msozeau
2008-04-16first-order --> firstorder (kills a warning about not being a valid id)letouzey
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 06:07:52 +0000