aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
AgeCommit message (Expand)Author
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
2008-04-04A file that can be loaded when a migration from Set to Type is desiredletouzey
2008-04-03New file FMapFullAVL containing the balancing proofs about FMapAVL:letouzey
2008-03-27Various fixes on typeclasses:msozeau
2008-03-20Installation des .vo nécessaire à BigQnotin
2008-03-19migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...letouzey
2008-03-16Ajout cible programs comme synonyme de subtacherbelin
2008-03-16Reorganize Program and Classes theories. Requiring Setoid no longer setsmsozeau
2008-03-15Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)letouzey
2008-03-11tactique Gappa : mise en placefilliatr
2008-03-08Fix bugs that were reopened due to the change of setoidmsozeau
2008-03-06Plug the new setoid implemtation in, leaving the original one commentedmsozeau
2008-02-26Proper implicit arguments handling for assumptionsmsozeau
2008-02-22Merge with lmamane's private branch:lmamane
2008-02-20Petits oublis dans Makefile.docnotin
2008-02-14Plongement de doc/Makefile dans la nouvelle architecutre des Makefilenotin
2008-02-13Move class_setoid to class_tactics.msozeau
2008-02-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
2008-02-04Reorganization of FSet+FMap : no more files specific to Weak Sets/Mapsletouzey
2008-02-03Add new files theories/Program/Basics.v and theories/Classes/Relations.vmsozeau
2008-02-02factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...letouzey
2008-01-24Prove the decidability of arithmetical statements using the real numbers.roconnor
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 12:56:57 +0000