index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
config/revision.ml, git: handle case when not at tip of a branch
lmamane
2009-02-11
*
clean: revision is now called config/revision.ml
lmamane
2009-02-11
*
Convert all uses of FIND_VCS_CLAUSE to recommended style
lmamane
2009-02-11
*
Cyclic31: proof of a forgotten admit
letouzey
2009-02-10
*
removed prehistoric files
barras
2009-02-10
*
man page of coqchk
barras
2009-02-10
*
Correction bug coqdev Hermann lehener.
soubiran
2009-02-10
*
commited complexity test for exponential behavior of unification
barras
2009-02-09
*
memoized is_ground_env
barras
2009-02-09
*
pushed evar reduction in kernel
barras
2009-02-06
*
Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]
herbelin
2009-02-06
*
Fixing #2044 (bad printing of primitive notation at the head of
herbelin
2009-02-06
*
From v8.2 to trunk:
herbelin
2009-02-06
*
Fix [subrelation] clauses that privileged the weakest. Better impl args
msozeau
2009-02-04
*
Report r11631 from 8.2 and handle non-dependent goals better in
msozeau
2009-02-04
*
Fix d'un bug avec l'option gallina
notin
2009-02-04
*
Do not reserve the keyword "Infer".
puech
2009-02-03
*
Allow to turn contrib/subtac into a (nat)dynlink'able plugin
letouzey
2009-02-03
*
Fix the installation of plugins (both initial and late ones)
letouzey
2009-02-03
*
Reorder coqmktop options and document -echo
glondu
2009-01-31
*
More portable way to pipe stderr
glondu
2009-01-30
*
Correction bug 2037.
soubiran
2009-01-30
*
Solves some warning and hides some not-bad ones in doc. It remains a
herbelin
2009-01-29
*
FSet(Weak)List : eq_dec becomes Defined (and gets better proof)
letouzey
2009-01-28
*
- Fixed various Overfull in documentation.
herbelin
2009-01-27
*
Cleaned CHANGES (rough backport of 11855 from v8.2 to trunk).
herbelin
2009-01-27
*
Forgot a file in r11859. Sorry...
puech
2009-01-27
*
Revert changes in pcoq functions to restore compatibility with contribs
puech
2009-01-26
*
Suppression de l'ancien logo (problèmes de droits)
notin
2009-01-23
*
Really compare evar maps in progress, due to merging in apply and other
msozeau
2009-01-23
*
Petit nettoyage faisant suite au commit #11847 .
aspiwack
2009-01-23
*
Fix #2011 : an incorrect environment when extracting Module ... with ...
letouzey
2009-01-22
*
Util.split_at : for quadratic to linear complexity
letouzey
2009-01-22
*
Extraction Library works now when some files share the same short name (fix #...
letouzey
2009-01-22
*
Fixes in the documentation of [dependent induction] and test-suite
msozeau
2009-01-22
*
configure: more adequate message explaining what -opt is doing
letouzey
2009-01-22
*
Fix d'un petit problème avec ocamlmklib en présence de l'option -camldir
notin
2009-01-22
*
Remplacement de cp --parents par un script sh
notin
2009-01-22
*
Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824
herbelin
2009-01-21
*
Fix bug #2004 due to bad handling of evars in the unification for
msozeau
2009-01-21
*
- Better deal with commands inside section titles in latex output using
msozeau
2009-01-21
*
Fixing bug #1918 (no occur-check in Meta unification was done yet!).
herbelin
2009-01-20
*
- Fixing bug 1891 (abusive instantiations of evar arguments in
herbelin
2009-01-20
*
Fixing a bug in 11804 (support for _ in ident entry of notations).
herbelin
2009-01-20
*
Added some missing statements for proof folding and corrected
vgross
2009-01-20
*
Added proof folding into CoqIde. See RefMan for using it.
vgross
2009-01-20
*
Cette version là fonctionne correctement au moins pour certaines
aspiwack
2009-01-20
*
More fixes...
aspiwack
2009-01-20
*
Un fix sur le commit précédent.
aspiwack
2009-01-20
*
Patch de l'installation:
aspiwack
2009-01-20
[prev]
[next]