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
*
Improved handling of element equalities in fsetdec (fix #2467)
letouzey
2011-10-07
*
ocamlbuild: remove -dllpath from coqrunbyteflags
glondu
2011-10-07
*
ocamlbuild: Fix ocamlbuild compilation for changes to configure from r14500.
glondu
2011-10-07
*
Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).
herbelin
2011-10-05
*
When a pattern match, don't use the first matching term but an
herbelin
2011-10-05
*
Removing vernacular code mistakenly committed.
herbelin
2011-10-05
*
Fixing critical inductive polymorphism bug found by Bruno.
herbelin
2011-10-05
*
Force dependency of Reference-Manual.pdf over Reference-Manual.dvi
herbelin
2011-10-05
*
Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...
letouzey
2011-10-05
*
It happens that the type inference algorithm (pretyping) did not check
herbelin
2011-10-05
*
Hash-consing of constr could share more
letouzey
2011-10-02
*
Updating some links in the FAQ
herbelin
2011-10-01
*
Moving never-used comments from Zhints.v to dev/doc so as not to
herbelin
2011-10-01
*
Fixing critical part of bug #2504. Not all inductive types in Type are
herbelin
2011-10-01
*
In Coq_config: get rid of coqsrc and make coqlib optional
glondu
2011-09-27
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
Generalizing subst_term_occ so that it supports an arbitrary matching
herbelin
2011-09-26
*
Adding subst_term up to conv
herbelin
2011-09-26
*
Moving implicit tactic support from Tacinterp to Pfedit and final evar
herbelin
2011-09-26
*
Polishing commits r14492, r14448 and r14407 (tactics propagate
herbelin
2011-09-25
*
Not hard-wiring camlp5 path in target source-doc!
herbelin
2011-09-25
*
Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev about
herbelin
2011-09-24
*
Completing r14448 and thus continuing r14407 (using Cast to propagate
herbelin
2011-09-24
*
Fix commit 14489: missing Coq. in dirpath
letouzey
2011-09-23
*
auto with nocore : disable the use of the core database (wish #2188)
letouzey
2011-09-23
*
Program: add some check_required_library (fix #2592) + some dead code removal
letouzey
2011-09-23
*
Remove specific hash-consing of Term.types (was unused anyway)
letouzey
2011-09-22
*
Hash-consing: attempt to stop hash-consing separately constr in declare.ml
letouzey
2011-09-22
*
Remove duplicated version of check_required_library.
letouzey
2011-09-22
*
test-suite : an additional message displayed by Notation2.v
letouzey
2011-09-22
*
Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.
letouzey
2011-09-22
*
Fixing bug #2606 (bad coqdoc processing of coq escaped in comments).
herbelin
2011-09-22
*
Makefile.doc: typo, index_url.txt should be index_urls.txt
letouzey
2011-09-19
*
Fix test-suite/ide for repository compiled without -local (fix #2600)
letouzey
2011-09-19
*
avoid dependency nightmare by creating coqdep_{lexer,common}.mli
letouzey
2011-09-18
*
doc/refman/Extraction.tex: no need to actually build euclid.ml
letouzey
2011-09-17
*
Euclid: make the proof transparent (example of extraction in stdlib)
letouzey
2011-09-17
*
Various fixes in the Makefiles
letouzey
2011-09-17
*
Omega: for non-arithmetical goals, try proving False from context (wish #2236)
letouzey
2011-09-16
*
Omega aware of Z.pred (fix #1912)
letouzey
2011-09-15
*
Re-allowing assumptions during proofs seems safe now (fix #2411)
letouzey
2011-09-15
*
coqc: Recognize option -force-load-proofs.
letouzey
2011-09-15
*
Names.make_mbid and co : convert from/to identifier (avoid some String.copy)
letouzey
2011-09-15
*
Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...
aspiwack
2011-09-12
*
correction du bug 2047
jforest
2011-09-09
*
More twicks on hash-consing
letouzey
2011-09-08
*
Fix the hconsing of universes
letouzey
2011-09-07
*
make world now builds fake_ide (to please coq-bench)
letouzey
2011-09-06
*
Improved ltac code for zify (fix #2575).
letouzey
2011-09-06
*
test-suite/ide: misc improvement
letouzey
2011-09-06
[next]