index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
Commit message (
Expand
)
Author
Age
*
Update changelogs
glondu
2011-02-11
*
Factorize code of rewrite to make way for a new implementation using the
msozeau
2011-02-07
*
Remove obsolete script univdot, update dev doc about universes
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Prepare change of nomenclature rawconstr -> glob_constr
glondu
2010-12-23
*
Print universes in debugging printers
glondu
2010-11-08
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Remove Explain* vernacs
glondu
2010-10-06
*
Install a printer for fconstr (ppconstr was installed twice)
glondu
2010-10-04
*
Simplify tactic(_)-bound arguments in TACTIC EXTEND rules
glondu
2010-09-30
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Updated COPYRIGHT file and header. Improved and fixed header updater.
herbelin
2010-07-24
*
Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).
herbelin
2010-07-22
*
Turned off Mac dynlink hack for 10.6.3+ on x86_64
thutchin
2010-07-05
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Names: remove obsolete mod_self_id
letouzey
2010-06-23
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Quick fix for having clenv debug printer working in trunk.
herbelin
2010-06-18
*
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
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Added debugging printer for the idmap used at evar definition time for
herbelin
2010-06-12
*
Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.
herbelin
2010-06-09
*
Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)
glondu
2010-06-07
*
Updated performance analysis file
herbelin
2010-06-06
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Nicer representation of tokens, more independant of camlp*
letouzey
2010-05-19
*
Improved the efficiency of evars traverals thanks to a split of
herbelin
2010-05-13
*
ocamldoc related fixes
pboutill
2010-05-03
*
"make source-doc" builds documentation of mli in html and pdf at
pboutill
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
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
*
Makefile: make devdocclean was not removing *.dep.ps, btw let's remove *.dep....
letouzey
2010-03-04
*
Remove bashisms
glondu
2010-01-28
*
Added module sharing support for typeclasses and hints (pri_auto_tactic).
soubiran
2010-01-12
*
* Segmenttree: New. A very simple implementation of segment trees.
regisgia
2010-01-08
*
Few misc. updates.
herbelin
2010-01-04
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
* Rewrite [classify_unicode] using standard unicode tables.
regisgia
2009-12-20
*
Addition of mergesort + cleaning of the Sorting library
herbelin
2009-12-13
*
Remove interface plugin
glondu
2009-12-02
*
Remove useless ppevd (which is identical to ppevm)
glondu
2009-11-13
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Fixed bug #2168 (closing a section may have as side-effect the erasure
herbelin
2009-11-11
[next]