aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* Cleaning of Nametab continued + fixed a compilation bug in previous commit.Gravatar herbelin2009-08-06
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Support for binding Coq root read-only in -R optionGravatar herbelin2009-07-01
* propagation sur le trunk du commit 12101 Gravatar soubiran2009-06-26
* Add doc for [Print Opaque Dependencies] and a better explanation for theGravatar msozeau2009-06-26
* Prevent automatic inference of implicit arguments when the auto flag isGravatar msozeau2009-06-01
* Fix extract hyps to correctly discharge all hyps as described by keepGravatar msozeau2009-05-29
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* Backporting 12080 (fixing bug #2091 on bad rollback in the "where"Gravatar herbelin2009-04-24
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* correction bug 2085Gravatar soubiran2009-04-06
* 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