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
*
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
*
Improving abbreviations/notations + backtrack of semantic change in r12439
herbelin
2009-11-11
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Fixed "Scheme Equality" when another instance of the scheme on the
herbelin
2009-11-08
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Fixed clash names in Relations (see bug report #2152) and make names
herbelin
2009-10-08
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Mise à jour du document de révision de la stdlib et déplacement de la
herbelin
2009-08-14
*
Fixed incorrect optimization in Prettyp.pr_located_qualid introduced
herbelin
2009-08-07
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
ocamldebug-coq: add some forgotten -I
letouzey
2009-05-26
*
Moved and completed the history of Coq versions from the
herbelin
2009-05-24
*
- Fixing declarative mode in presence of high use of Change_evars nodes
herbelin
2009-05-20
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
- Cleaning (unification of ML names, removal of obsolete code,
herbelin
2009-04-27
[next]