index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
funind
Commit message (
Expand
)
Author
Age
*
Fixed incorrect computation of possible guard in presence of `{ ... } contexts.
herbelin
2009-12-12
*
Updated compatibility for rewriting equality proofs that are dependent
herbelin
2009-12-12
*
Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...
letouzey
2009-12-09
*
Continuing r12485-12486 and r12549 (cleaning around name generation)
herbelin
2009-12-02
*
Continuing r12485-12486 (cleaning around name generation)
herbelin
2009-12-01
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
Added support for multiple where-clauses in Inductive and co (see wish #2163).
herbelin
2009-11-11
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
gmelquio
2009-11-04
*
OrderedType implementation for various numerical datatypes + min/max structures
letouzey
2009-11-03
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Fixed small name freshness bug in Functional Scheme ("Heq" name was
herbelin
2009-10-03
*
Remove useless Liboject.export_function field
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
repport of commit r12221
jforest
2009-07-04
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20