aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Makefile: don't mention bin/coqtop.byte twice to make when BEST=byte, it comp...Gravatar lmamane2007-07-18
* Cleanly refuse to operate in the presence of unsaved changes in emacsGravatar lmamane2007-07-18
* Affichage de "thesis" seulement en mode déclaratifGravatar herbelin2007-07-18
* Oups... Use shell-variable syntax in shell commands.Gravatar lmamane2007-07-18
* Makefile: Revert r10015, which was based on a misunderstandingGravatar lmamane2007-07-18
* Raffinement de interp_ident pour que l'ident interprété soit au choixGravatar herbelin2007-07-18
* Makefile: needs GNU Make 3.81Gravatar lmamane2007-07-18
* J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir Gravatar aspiwack2007-07-18
* Makefile: more robustness all aroundGravatar lmamane2007-07-18
* Makefile: Do _not_ delete dummy .ml files of .ml4 files even when not needed ...Gravatar lmamane2007-07-17
* Do not try to clean the doc when no config/MakefileGravatar lmamane2007-07-16
* Reorganise cleaning targetsGravatar lmamane2007-07-16
* Makefile: -MG doesn't (and can't) do what is necessaryGravatar lmamane2007-07-16
* A cleaner solution to "make deletes .ml4.d files -> infinite loop" problemGravatar lmamane2007-07-16
* Oups... empty .ml4.d files producedGravatar lmamane2007-07-16
* CAMLP4DEPS will not work for .byteml and .optmlGravatar lmamane2007-07-16
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* Makefile: work around gcc bug: lhs of make rule created by -MM does not inclu...Gravatar lmamane2007-07-16
* Makefile: in C, .d files need to depend on the same as the .o fileGravatar lmamane2007-07-16
* makefile: dependencies of .c files: assume missing headers are generated filesGravatar lmamane2007-07-16
* Makefile: use CFLAGS for dependency generation of .c filesGravatar lmamane2007-07-15
* An update on axiomatization of number classes.Gravatar emakarov2007-07-13
* some more useless constant in const_omegaGravatar letouzey2007-07-13
* Beginning of a reorganisation of the ml part for romega: Gravatar letouzey2007-07-13
* A emacs-specific comment to use makefile-mode on Makefile.*Gravatar letouzey2007-07-13
* Added Qpower_plus' and Zpower_QpowerGravatar roconnor2007-07-13
* Small cleanupGravatar letouzey2007-07-13
* Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans leGravatar herbelin2007-07-13
* Deletion of some firstorder calls in FSetAVL: Gravatar letouzey2007-07-13
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
* removing a warning at compilation timeGravatar jforest2007-07-13
* Proof for subGravatar thery2007-07-12
* (Port of r9984) Easier debugging:Gravatar glondu2007-07-12
* Update (test-suite was not successful).Gravatar glondu2007-07-12
* Deletion of an obsolete file (euclidian division done in old syntax with real...Gravatar letouzey2007-07-12
* Deletion of contrib/extraction/testGravatar letouzey2007-07-12
* normalisation (by closure) was not performed under fixpointsGravatar barras2007-07-12
* port de r9968: bug avec les ring calculatoiresGravatar barras2007-07-12
* An optimization to simplify generated obligations removing unnecessary let-in's.Gravatar msozeau2007-07-12
* Fix bug when adding progs with no obligationsGravatar msozeau2007-07-12
* Forgot to commit new MakefileGravatar msozeau2007-07-12
* Remove dead modules in Subtac.Gravatar msozeau2007-07-12
* Cleanup, use Util list functions when possibleGravatar msozeau2007-07-12
* Proof for succ, add, predGravatar thery2007-07-12
* dead codeGravatar letouzey2007-07-11
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
* Added ForAll_Str_nth_tlGravatar roconnor2007-07-11
* Big reorganization of romega/ReflOmegaCore.v: towards a modular Gravatar letouzey2007-07-10
* Petites corrections sur le MakefileGravatar notin2007-07-09
* More natural notation for intro pattern: @a -> ?aGravatar glondu2007-07-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-16 14:45:20 +0000