index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
/
doc
Commit message (
Expand
)
Author
Age
*
Fix a typo in dev/doc/changes.txt
Jason Gross
2016-03-04
*
Update history of revisions.
Hugo Herbelin
2015-12-02
*
Being more precise and faithful about the origin of the file reporting
Hugo Herbelin
2015-11-16
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Minor typo in universe polymorphism doc.
Maxime Dénès
2015-10-09
*
Updating versions history with data from Gérard.
Hugo Herbelin
2015-10-02
*
Update the history of versions with recent versions.
Hugo Herbelin
2015-10-02
*
Univs: More info for developers.
Matthieu Sozeau
2015-10-02
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
A reorganization of the "assert" tactics (hopefully uniform naming
Hugo Herbelin
2014-08-18
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
Moved code for finding subterms (pattern, induction, set, generalize, ...)
Hugo Herbelin
2014-06-28
*
Change Ltac constr matching semantics to consider universes when merging two
Matthieu Sozeau
2014-06-15
*
A little bit of documentation about V5.10 and V6.3 and V7.
Hugo Herbelin
2014-06-01
*
Isolating a function "make_abstraction", new name of "letin_abstract",
Hugo Herbelin
2014-05-08
*
Renaming new_induct -> induction; new_destruct -> destruct.
Hugo Herbelin
2014-05-08
*
Add incompatibilities paragraph in doc about universe polymorphism.
Matthieu Sozeau
2014-05-06
*
Add doc on the new API for universe polymorphism and primitive projections
Matthieu Sozeau
2014-05-06
*
Set officially the minimal OCaml requirement to 3.12.1
Pierre Letouzey
2014-03-02
*
Makefile: re-introduce 2 phases to avoid make strange -include's
Pierre Letouzey
2014-02-27
*
A file listing old svn branches and tags
letouzey
2013-11-18
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
Revert "remove -rectypes except for term.ml"
mdenes
2013-01-22
*
remove -rectypes except for term.ml
letouzey
2012-10-06
*
Remove broken makefile option NO_RECOMPILE_LIB
letouzey
2012-09-20
*
Some documentation of recent changes concerning interfaces
letouzey
2012-05-29
*
debugging.txt: no more typing of #use "include" if using .ocamlinit
letouzey
2011-10-15
*
Moved to a more standard order of arguments (i.e. env followed by evar_map)
herbelin
2011-10-11
*
Moving never-used comments from Zhints.v to dev/doc so as not to
herbelin
2011-10-01
*
A few comments and a dev file to summarize issues with unification
herbelin
2011-06-13
*
Update changelogs
glondu
2011-02-11
*
Remove obsolete script univdot, update dev doc about universes
glondu
2010-12-24
*
Simplify tactic(_)-bound arguments in TACTIC EXTEND rules
glondu
2010-09-30
*
Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).
herbelin
2010-07-22
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Fixed commit 13125 (stricter check of induction args): an interpretation
herbelin
2010-06-14
*
Fixed a bug in pretty-printing "induction" and "destruct" due to a
herbelin
2010-06-13
*
Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.
herbelin
2010-06-09
*
Updated performance analysis file
herbelin
2010-06-06
*
Improved the efficiency of evars traverals thanks to a split of
herbelin
2010-05-13
*
Removing redundant internal variants of apply tactic and simplification of ML...
herbelin
2010-04-14
*
Added a function in typing.ml to solve evars of a constr w/o going back down ...
herbelin
2010-04-05
*
Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...
letouzey
2010-03-04
*
Few misc. updates.
herbelin
2010-01-04
*
Addition of mergesort + cleaning of the Sorting library
herbelin
2009-12-13
*
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 clash names in Relations (see bug report #2152) and make names
herbelin
2009-10-08
[next]