aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-08-10Typonotin
2007-08-10Modification de la test suite pour intégrer des tests spécifiques auxnotin
2007-08-09Modification de control_only_guard, qui utilise maintenantnotin
2007-08-08Fix dependency bugs due to Program modules renamings.msozeau
2007-08-08Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vemakarov
2007-08-08Add a test case for the new "dependent" induction tactics.msozeau
2007-08-08A better Program documentation. Include it in the generated stdlib doc.msozeau
2007-08-07Move Program tactics into a proper theories/ directory as they are general pu...msozeau
2007-08-07Add a new tactic to generalize an instantiated inductive predicate adding equ...msozeau
2007-08-07Build system: _really_ don't recurse into VCS metadata for file listslmamane
2007-08-07Build system:lmamane
2007-08-01Build system: BSD compatibility: do not use -printf action of findlmamane
2007-07-30mul and sqrtthery
2007-07-26Corrected the reference to glob.dump, which is used to create stdlib/index-bo...emakarov
2007-07-25Add glob.dump to Makefile the recommended way and document thelmamane
2007-07-25Modifications de la construction de la documentation de la librairienotin
2007-07-25Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n etnotin
2007-07-24fixed bug 1448 and 1674barras
2007-07-24proof of compare addedthery
2007-07-24fixed bug 1675: computing carrier from the relation type was not rightbarras
2007-07-24Declarative language: fixed the generation of fixpoints for induction proofs.corbinea
2007-07-24An update on axiomatization of numbers.emakarov
2007-07-23removed thesisbarras
2007-07-19Documentation of Program and its tactics, fix enormous interaction bug due to...msozeau
2007-07-19some more svn:ignore propertiesletouzey
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
2007-07-18Makefile: slightly cleaner version of r10026lmamane
2007-07-18Makefile: don't mention bin/coqtop.byte twice to make when BEST=byte, it comp...lmamane
2007-07-18Cleanly refuse to operate in the presence of unsaved changes in emacslmamane
2007-07-18Affichage de "thesis" seulement en mode déclaratifherbelin
2007-07-18Oups... Use shell-variable syntax in shell commands.lmamane
2007-07-18Makefile: Revert r10015, which was based on a misunderstandinglmamane
2007-07-18Raffinement de interp_ident pour que l'ident interprété soit au choixherbelin
2007-07-18Makefile: needs GNU Make 3.81lmamane
2007-07-18J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir aspiwack
2007-07-18Makefile: more robustness all aroundlmamane
2007-07-17Makefile: Do _not_ delete dummy .ml files of .ml4 files even when not needed ...lmamane
2007-07-16Do not try to clean the doc when no config/Makefilelmamane
2007-07-16Reorganise cleaning targetslmamane
2007-07-16Makefile: -MG doesn't (and can't) do what is necessarylmamane
2007-07-16A cleaner solution to "make deletes .ml4.d files -> infinite loop" problemlmamane
2007-07-16Oups... empty .ml4.d files producedlmamane
2007-07-16CAMLP4DEPS will not work for .byteml and .optmllmamane
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
2007-07-16Makefile: work around gcc bug: lhs of make rule created by -MM does not inclu...lmamane
2007-07-16Makefile: in C, .d files need to depend on the same as the .o filelmamane
2007-07-16makefile: dependencies of .c files: assume missing headers are generated fileslmamane
2007-07-15Makefile: use CFLAGS for dependency generation of .c fileslmamane
2007-07-13An update on axiomatization of number classes.emakarov
2007-07-13some more useless constant in const_omegaletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 08:05:45 +0000