index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Bug 2050, commit v8.2 11923-11924 ---> trunk
soubiran
2009-02-13
*
Correction bug coqdev Hermann lehener.
soubiran
2009-02-10
*
pushed evar reduction in kernel
barras
2009-02-06
*
Allow to turn contrib/subtac into a (nat)dynlink'able plugin
letouzey
2009-02-03
*
Correction bug 2037.
soubiran
2009-01-30
*
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
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
*
DISCLAIMER
puech
2009-01-17
*
Uniformisation of some error messages + added test on setoid rewrite.
herbelin
2009-01-07
*
Switched to "standardized" names for the properties of eq and
herbelin
2009-01-01
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
- coq_makefile: target install now respects the original tree structure
herbelin
2008-12-24
*
Correction d'un bug causant un Not_found dans la contrib FSet.
soubiran
2008-12-18
*
correction bug 1997.
soubiran
2008-11-25
*
- Synchronized subst_object with load_object (load_and_subst_objects)
herbelin
2008-11-23
*
Move Record desugaring to constrintern and add ability to use notations
msozeau
2008-11-05
*
Correction bug 1979.
soubiran
2008-10-28
*
Correction bug #1969.
soubiran
2008-10-21
*
Report des commits 11417 et 11437 de la v8.2
soubiran
2008-10-15
*
In manual implicit arguments mode, do not enrich implicits
msozeau
2008-09-14
*
moved magic numbers to configure (share coq/coqchk)
barras
2008-07-24
*
broke cyclic dependencies
barras
2008-07-24
*
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-07-22
*
Suite de la révision #11212
notin
2008-07-08
*
Fix implicit arguments in sections bug and check for resolution of evars when
msozeau
2008-07-07
*
Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...
notin
2008-07-07
*
Fixes in handling of implicit arguments:
msozeau
2008-07-04
*
Documentation Prop<=Set et Arguments Scope Global
herbelin
2008-07-01
*
Fichiers oubliés lors du 11188 :-(
herbelin
2008-06-30
*
Lissage de la gestion des chemins de chargement de fichiers :
herbelin
2008-06-29
*
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...
notin
2008-06-25
*
meilleur gestion de la fonction de "cache" des alias (declaremods), et correc...
soubiran
2008-06-18
*
Confusion sur commit précédent de library. La capture du Not_found
herbelin
2008-06-12
*
Bug dans l'adaptation de library_full_filename lors du débranchement
herbelin
2008-06-11
*
Correction bug alias d'alias.
soubiran
2008-06-11
*
- Documentation de admit et Print Assumptions.
herbelin
2008-06-09
*
Enhancements to coqdoc, better globalization of sections and modules.
msozeau
2008-06-06
*
ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...
soubiran
2008-06-06
*
Fix setoid_rewrite documentation examples.
msozeau
2008-06-03
*
Improvements on coqdoc by adding more information into .glob
msozeau
2008-05-30
*
- Prise en compte des frozen state de Coq autant que possible pour
herbelin
2008-05-24
*
Correction bug #1842 + correction bug initialisation introduit dans
herbelin
2008-05-10
*
- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des
herbelin
2008-05-10
*
** Efficacité, bugs, robustesse CoqIDE **
herbelin
2008-05-08
*
correction bug 1839
soubiran
2008-04-25
*
Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840
herbelin
2008-04-24
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
[next]