index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
- Fix handling of clauses in setoid_rewrite to rewrite under binders
msozeau
2009-04-17
*
comparison functions on lists and arrays
barras
2009-04-16
*
Fix bug #2089: correctly dealing with parameters and real arguments in
msozeau
2009-04-16
*
Better Requires in Classes. Fix bug #2093: the code does not require
msozeau
2009-04-16
*
nouvelle version de la tactique groebner proposee par Loic:
barras
2009-04-16
*
Rewrite autorewrite to use a dnet indexed by the left-hand sides (or
msozeau
2009-04-14
*
Add a combinator for rewriting given a list of terms and fix the
msozeau
2009-04-14
*
Correction du patch -rectypes pour ocaml 3.10
vsiles
2009-04-14
*
Some additions in Max and Zmax. Unifiying list of statements and names
herbelin
2009-04-14
*
Fix and actually beautify the bug script to adapt to the new measure
msozeau
2009-04-14
*
Rewrite of setoid_rewrite to modularize it based on proof-producing
msozeau
2009-04-13
*
Fix premature optimisation in dependent induction: even variable args need
msozeau
2009-04-10
*
Fix tauto no longer failing after commit 12077; appropriate error
herbelin
2009-04-10
*
Turning tauto into a classical tautology prover as soon as classical
herbelin
2009-04-09
*
Backtrack on 12061 (type checking for bug #2084 too strong as soon as we use
herbelin
2009-04-09
*
ocamlbuild: right symlink for csdpcert
letouzey
2009-04-08
*
Take formatted into account in rules for dot.
msozeau
2009-04-08
*
Experimental support for automatic destruction of recursive calls and
msozeau
2009-04-08
*
Fix bug #2083 for good: verify that the measure and relation are
msozeau
2009-04-08
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
ocamlbuild: tags for new file tactics/rewrite.ml4
letouzey
2009-04-08
*
Change HTML paragraph output to avoid too much space after bulleted
msozeau
2009-04-08
*
Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branch
herbelin
2009-04-08
*
- Fixing bug #2084 (unification not checking sort constraints), hoping
herbelin
2009-04-08
*
A first pearl found by the Oug analyzer: there were two list_map_i in Util
letouzey
2009-04-08
*
- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing
herbelin
2009-04-08
*
Fixes in Program:
msozeau
2009-04-07
*
Move setoid_rewrite to its own module and do some clean up in
msozeau
2009-04-07
*
Fix behavior on newlines with parse-comments and also do [] escaping as
msozeau
2009-04-06
*
correction bug 2085
soubiran
2009-04-06
*
Display the content of the list instead of "<list>" when an idtac
herbelin
2009-04-05
*
Fix obvious bug in evars_of_named_context.
msozeau
2009-04-03
*
Ocamlbuild: option for (not) building coqide, better log messages
letouzey
2009-04-03
*
Makefile: ocamlbuild's _build is not traversed by find, and removed by make c...
letouzey
2009-04-03
*
Ocamlbuild: improvements suggested by N. Pouillard
letouzey
2009-04-03
*
Fix auto so that Extern tactics associated to no patterns can apply to
msozeau
2009-03-31
*
Committed patch sent by Samuel Bronson on Mar 14 2009 to take care of
herbelin
2009-03-31
*
Complementary fix to have ocamlopt_shared_os5fix.sh working correctly
herbelin
2009-03-31
*
Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)
letouzey
2009-03-30
*
Update CHANGES
glondu
2009-03-30
*
Document new quote construction
glondu
2009-03-30
*
Add tests for quote
glondu
2009-03-30
*
Add a more general quote construction
glondu
2009-03-30
*
Fix some typos and spaces
glondu
2009-03-30
*
Csdpcert: adaptation after last commit
letouzey
2009-03-29
*
Micromega: improvement of the code obtained by extraction
letouzey
2009-03-29
*
ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)
letouzey
2009-03-29
*
Avoid inadvertent declaration of "on" as a keyword. New syntax is
msozeau
2009-03-29
*
Fix useless redeclaration of a tactic name when UpdateTac is replayed.
msozeau
2009-03-28
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
[prev]
[next]