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
*
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
*
Mise à jour du document de révision de la stdlib et déplacement de la
herbelin
2009-08-14
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Moved and completed the history of Coq versions from the
herbelin
2009-05-24
*
- 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
*
Correction du patch -rectypes pour ocaml 3.10
vsiles
2009-04-14
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20
*
Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)
herbelin
2009-03-17
*
Cleaning/uniformizing the interface of tacticals.mli
herbelin
2009-03-14
*
#rectypes was already automatically added when using 3.11
herbelin
2009-02-17
*
Made hack to have Drop and #use"include" working with ocaml 3.10 public
herbelin
2009-02-17
*
Document how FIND_VCS_CLAUSE has to be used
lmamane
2009-02-11
*
- Structuring Numbers and fixing Setoid in stdlib's doc.
herbelin
2009-01-19
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
About "apply in":
herbelin
2008-12-09
*
Use $(COQTOPEXE) to refer to bin/coqtop in Makefiles
glondu
2008-09-06
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
MAJ diverses
herbelin
2008-06-11
*
- Patch sur "intros until 0"
herbelin
2008-06-08
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Fix typos
lmamane
2008-06-05
*
- Correction bug highlighting "Module" dans Coqide
herbelin
2008-05-28
*
Mise en place d'un algorithme d'inversion des contraintes de type lors
herbelin
2008-05-05
*
Quelques éléments de réflexion
herbelin
2008-05-03
*
Correction du bug des types singletons pas sous-type de Set
herbelin
2008-04-27
*
Chgts mineurs:
herbelin
2008-04-03
*
Implement KEEP_ML4_PREPROCESSED option in build system
lmamane
2008-02-13
*
Implement NO_RECALC_DEPS option in build system
lmamane
2008-02-13
*
MAJ
herbelin
2007-10-29
*
Allow a few build system optimisations/corner-cutting
lmamane
2007-10-11
*
Add glob.dump to Makefile the recommended way and document the
lmamane
2007-07-25
*
Reorganise cleaning targets
lmamane
2007-07-16
*
A cleaner solution to "make deletes .ml4.d files -> infinite loop" problem
lmamane
2007-07-16
*
New bootstrapping, improved, Makefile system
corbinea
2007-07-13
*
MAJ
herbelin
2007-05-21
[next]