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
*
Ajout de la gestion de Local et Global pour les options (au sens de
aspiwack
2009-08-14
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
Fixed incorrect optimization in Prettyp.pr_located_qualid introduced
herbelin
2009-08-07
*
Cleaning of Nametab continued + fixed a compilation bug in previous commit.
herbelin
2009-08-06
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Support for binding Coq root read-only in -R option
herbelin
2009-07-01
*
propagation sur le trunk du commit 12101
soubiran
2009-06-26
*
Add doc for [Print Opaque Dependencies] and a better explanation for the
msozeau
2009-06-26
*
Prevent automatic inference of implicit arguments when the auto flag is
msozeau
2009-06-01
*
Fix extract hyps to correctly discharge all hyps as described by keep
msozeau
2009-05-29
*
Fix implicit args code so that declarations are added for all
msozeau
2009-05-27
*
Stop using a "Manual Implicit Arguments" flag and support them as soon
msozeau
2009-05-27
*
Backporting 12080 (fixing bug #2091 on bad rollback in the "where"
herbelin
2009-04-24
*
Fix premature optimisation in dependent induction: even variable args need
msozeau
2009-04-10
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
correction bug 2085
soubiran
2009-04-06
*
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
[next]