aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2007-07-13Beginning of a reorganisation of the ml part for romega: letouzey
2007-07-13A emacs-specific comment to use makefile-mode on Makefile.*letouzey
2007-07-13Added Qpower_plus' and Zpower_Qpowerroconnor
2007-07-13Small cleanupletouzey
2007-07-13Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans leherbelin
2007-07-13Deletion of some firstorder calls in FSetAVL: letouzey
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
2007-07-13removing a warning at compilation timejforest
2007-07-12Proof for subthery
2007-07-12(Port of r9984) Easier debugging:glondu
2007-07-12Update (test-suite was not successful).glondu
2007-07-12Deletion of an obsolete file (euclidian division done in old syntax with real...letouzey
2007-07-12Deletion of contrib/extraction/testletouzey
2007-07-12normalisation (by closure) was not performed under fixpointsbarras
2007-07-12port de r9968: bug avec les ring calculatoiresbarras
2007-07-12An optimization to simplify generated obligations removing unnecessary let-in's.msozeau
2007-07-12Fix bug when adding progs with no obligationsmsozeau
2007-07-12Forgot to commit new Makefilemsozeau
2007-07-12Remove dead modules in Subtac.msozeau
2007-07-12Cleanup, use Util list functions when possiblemsozeau
2007-07-12Proof for succ, add, predthery
2007-07-11dead codeletouzey
2007-07-11Slight cleanup of refl_omega.ml : in particular it uses now listletouzey
2007-07-11Added ForAll_Str_nth_tlroconnor
2007-07-10Big reorganization of romega/ReflOmegaCore.v: towards a modular letouzey
2007-07-09Petites corrections sur le Makefilenotin
2007-07-09More natural notation for intro pattern: @a -> ?aglondu
2007-07-09Improvements / Bug fixes for ROmega letouzey
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
2007-07-06a few works about my commits since Februaryletouzey
2007-07-06minor bug correction (continuing r 9943)jforest
2007-07-06Update of theories/Numbers directory.emakarov
2007-07-06Adding a syntax for "n-ary" rewrite: letouzey
2007-07-06sequel to commit 9952: forgot to adapt xlate to the new n-ary renameletouzey
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 20:13:30 +0000