aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2009-04-27Cleanup old eauto code.msozeau
2009-04-27- Implementation of a new typeclasses eauto procedure based on successmsozeau
2009-04-27- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-04-24Report de la révision #12104 (Maj lien site web de Coq)notin
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
2009-04-24Fixing bug #2308 ("instantiate" tactic did not comply withherbelin
2009-04-24- New cleaning phase for the entry points of pretyping.mlherbelin
2009-04-21fixed CBV strategy: it was too eager on terms likebarras
2009-04-21Rename [Morphism] into [Proper] and [respect] into [proper] to complymsozeau
2009-04-20Fix test output mentionning an existential number that changed.msozeau
2009-04-20Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact thatmsozeau
2009-04-18Just export RelationClasses for [Equivalence] through Setoid.msozeau
2009-04-17Only export the notations of Morphism as well as Equivalence throughmsozeau
2009-04-17- Fix handling of clauses in setoid_rewrite to rewrite under bindersmsozeau
2009-04-16comparison functions on lists and arraysbarras
2009-04-16Fix bug #2089: correctly dealing with parameters and real arguments inmsozeau
2009-04-16Better Requires in Classes. Fix bug #2093: the code does not requiremsozeau
2009-04-16nouvelle version de la tactique groebner proposee par Loic:barras
2009-04-14Rewrite autorewrite to use a dnet indexed by the left-hand sides (ormsozeau
2009-04-14Add a combinator for rewriting given a list of terms and fix themsozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 22:52:28 +0000