index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Fix de divers petits problèmes d'installation
notin
2009-02-11
*
Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin
2009-02-11
*
Allow to turn contrib/subtac into a (nat)dynlink'able plugin
letouzey
2009-02-03
*
Revert changes in pcoq functions to restore compatibility with contribs
puech
2009-01-26
*
Petit nettoyage faisant suite au commit #11847 .
aspiwack
2009-01-23
*
Les records déclarés avec Record ne peuvent plus être récursifs (le
aspiwack
2009-01-19
*
- Structuring Numbers and fixing Setoid in stdlib's doc.
herbelin
2009-01-19
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
*
Getting rid of the previous implementation of setoid_rewrite which was
msozeau
2009-01-18
*
Last changes in type class syntax:
msozeau
2009-01-18
*
DISCLAIMER
puech
2009-01-17
*
Fixing #1960 (xml bug with external on goal variable) and #1961
herbelin
2009-01-14
*
Fixing/improving management of uniform prefix Local and Global
herbelin
2009-01-14
*
- Standardized prefix use of "Local"/"Global" modifiers as decided in
herbelin
2009-01-13
*
- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).
herbelin
2009-01-11
*
Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...
notin
2009-01-06
*
Completed 11745 (move of jprover to user contribs) and cleaned 11743
herbelin
2009-01-05
*
Bug dans commit 11743
herbelin
2009-01-04
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
Made the debugger work again:
herbelin
2009-01-02
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
- Suppression date dans configure du trunk
herbelin
2008-12-26
*
- coq_makefile: target install now respects the original tree structure
herbelin
2008-12-24
*
Nettoyage des variables Coq et amélioration de coqmktop. Les
notin
2008-12-19
*
Sequel of 11697: repair coqtop.byte when contribs are statically linked (+min...
letouzey
2008-12-17
*
Take advantage of natdynlink when available: almost all contribs become loada...
letouzey
2008-12-16
*
Generalized binding syntax overhaul: only two new binders: `() and `{},
msozeau
2008-12-14
*
About "apply in":
herbelin
2008-12-09
*
Correct handling of defined methods (let-ins) in instance declarations.
msozeau
2008-12-04
*
Inductive parameters: nicer doc examples and error message
letouzey
2008-11-28
*
- Synchronized subst_object with load_object (load_and_subst_objects)
herbelin
2008-11-23
*
Minor improvement to commit 11619
herbelin
2008-11-23
*
Fixed bug #2006 (type constraint on Record was not taken into account) +
herbelin
2008-11-23
*
Fixed bug in VernacExtend printing + missing vernacular printing rules +
herbelin
2008-11-22
*
- Fixed minor bug #1994 in the tactic chapter of the manual [doc]
herbelin
2008-11-22
*
Tentative d'amélioration de la robustesse des Makefile générés par
notin
2008-11-13
*
Fix mixup between Record, Structure and Class by adding a new variant for
msozeau
2008-11-10
*
More factorization of inductive/record and typeclasses: move class
msozeau
2008-11-09
*
- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in
herbelin
2008-11-09
*
Slight change of the semantics of user-given casts: they don't really
msozeau
2008-11-07
*
Fix in the unification algorithm using evars: unify types of evar
msozeau
2008-11-05
*
Move Record desugaring to constrintern and add ability to use notations
msozeau
2008-11-05
*
Petit bug dans le commit précédent.
aspiwack
2008-11-05
*
Nouvelle syntaxe pour écrire des records (co)inductifs :
aspiwack
2008-11-05
*
Remove calls to Dynlink.add_{interfaces,available_units} altogether
glondu
2008-10-29
*
Native "Declare ML Module" when possible
glondu
2008-10-28
*
11511 continued (bug in set.out + incohérence dans "Theorem with"
herbelin
2008-10-28
*
- Fixed many "Theorem with" bugs.
herbelin
2008-10-27
*
Fixes and refinements regarding occurrence selection:
herbelin
2008-10-26
[next]