aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2009-04-14Correction du patch -rectypes pour ocaml 3.10vsiles
2009-04-14Some additions in Max and Zmax. Unifiying list of statements and namesherbelin
2009-04-14Fix and actually beautify the bug script to adapt to the new measuremsozeau
2009-04-13Rewrite of setoid_rewrite to modularize it based on proof-producingmsozeau
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
2009-04-10Fix tauto no longer failing after commit 12077; appropriate errorherbelin
2009-04-09Turning tauto into a classical tautology prover as soon as classicalherbelin
2009-04-09Backtrack on 12061 (type checking for bug #2084 too strong as soon as we useherbelin
2009-04-08ocamlbuild: right symlink for csdpcertletouzey
2009-04-08Take formatted into account in rules for dot.msozeau
2009-04-08Experimental support for automatic destruction of recursive calls andmsozeau
2009-04-08Fix bug #2083 for good: verify that the measure and relation aremsozeau
2009-04-08Some dead code removal + cleanupsletouzey
2009-04-08ocamlbuild: tags for new file tactics/rewrite.ml4letouzey
2009-04-08Change HTML paragraph output to avoid too much space after bulletedmsozeau
2009-04-08Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branchherbelin
2009-04-08- Fixing bug #2084 (unification not checking sort constraints), hopingherbelin
2009-04-08A first pearl found by the Oug analyzer: there were two list_map_i in Utilletouzey
2009-04-08- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingherbelin
2009-04-07Fixes in Program: msozeau
2009-04-07Move setoid_rewrite to its own module and do some clean up inmsozeau
2009-04-06Fix behavior on newlines with parse-comments and also do [] escaping as msozeau
2009-04-06correction bug 2085soubiran
2009-04-05Display the content of the list instead of "<list>" when an idtacherbelin
2009-04-03Fix obvious bug in evars_of_named_context.msozeau
2009-04-03Ocamlbuild: option for (not) building coqide, better log messagesletouzey
2009-04-03Makefile: ocamlbuild's _build is not traversed by find, and removed by make c...letouzey
2009-04-03Ocamlbuild: improvements suggested by N. Pouillardletouzey
2009-03-31Fix auto so that Extern tactics associated to no patterns can apply tomsozeau
2009-03-31Committed patch sent by Samuel Bronson on Mar 14 2009 to take care ofherbelin
2009-03-31Complementary fix to have ocamlopt_shared_os5fix.sh working correctlyherbelin
2009-03-30Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)letouzey
2009-03-30Update CHANGESglondu
2009-03-30Document new quote constructionglondu
2009-03-30Add tests for quoteglondu
2009-03-30Add a more general quote constructionglondu
2009-03-30Fix some typos and spacesglondu
2009-03-29Csdpcert: adaptation after last commitletouzey
2009-03-29Micromega: improvement of the code obtained by extractionletouzey
2009-03-29ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)letouzey
2009-03-29Avoid inadvertent declaration of "on" as a keyword. New syntax ismsozeau
2009-03-28Fix useless redeclaration of a tactic name when UpdateTac is replayed.msozeau
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-28Fix bug #2056 (discharge bug).msozeau
2009-03-28Fix static compilation of numeral syntax (typo in _mod files, sorry ...)letouzey
2009-03-28ZArith/Int: no need to load romega here (but rather in FullAVL)letouzey
2009-03-28ZMicromega: useless dependency toward ZArith.Intletouzey
2009-03-27Coqdep: some dead code and code move (first experiment with Oug)letouzey
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
2009-03-27Remove unused mli filesletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 15:50:34 +0000