aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Bug 2050, commit v8.2 11923-11924 ---> trunkGravatar soubiran2009-02-13
* Correction bug coqdev Hermann lehener.Gravatar soubiran2009-02-10
* pushed evar reduction in kernelGravatar barras2009-02-06
* Allow to turn contrib/subtac into a (nat)dynlink'able pluginGravatar letouzey2009-02-03
* Correction bug 2037.Gravatar soubiran2009-01-30
* Petit nettoyage faisant suite au commit #11847 .Gravatar aspiwack2009-01-23
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* DISCLAIMERGravatar puech2009-01-17
* Uniformisation of some error messages + added test on setoid rewrite.Gravatar herbelin2009-01-07
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Correction d'un bug causant un Not_found dans la contrib FSet.Gravatar soubiran2008-12-18
* correction bug 1997.Gravatar soubiran2008-11-25
* - Synchronized subst_object with load_object (load_and_subst_objects)Gravatar herbelin2008-11-23
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Correction bug 1979.Gravatar soubiran2008-10-28
* Correction bug #1969.Gravatar soubiran2008-10-21
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* In manual implicit arguments mode, do not enrich implicitsGravatar msozeau2008-09-14
* moved magic numbers to configure (share coq/coqchk)Gravatar barras2008-07-24
* broke cyclic dependenciesGravatar barras2008-07-24
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Suite de la révision #11212Gravatar notin2008-07-08
* Fix implicit arguments in sections bug and check for resolution of evars whenGravatar msozeau2008-07-07
* Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...Gravatar notin2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Documentation Prop<=Set et Arguments Scope GlobalGravatar herbelin2008-07-01
* Fichiers oubliés lors du 11188 :-(Gravatar herbelin2008-06-30
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* meilleur gestion de la fonction de "cache" des alias (declaremods), et correc...Gravatar soubiran2008-06-18
* Confusion sur commit précédent de library. La capture du Not_foundGravatar herbelin2008-06-12
* Bug dans l'adaptation de library_full_filename lors du débranchementGravatar herbelin2008-06-11
* Correction bug alias d'alias.Gravatar soubiran2008-06-11
* - Documentation de admit et Print Assumptions.Gravatar herbelin2008-06-09
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...Gravatar soubiran2008-06-06
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* - Prise en compte des frozen state de Coq autant que possible pourGravatar herbelin2008-05-24
* Correction bug #1842 + correction bug initialisation introduit dansGravatar herbelin2008-05-10
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* correction bug 1839Gravatar soubiran2008-04-25
* Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840Gravatar herbelin2008-04-24
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23