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
*
Backtrack sur la mémoïsation de nf_evar.
aspiwack
2009-03-04
*
Temporary hack to make coqide.byte work (backport r11948) (see #2062)
glondu
2009-03-04
*
fixes to typecheck with old lablgtk.
vgross
2009-03-04
*
Hack to fix compilation problems. will be removed on lablgtk upgrade.
vgross
2009-03-03
*
porting r11900 11905 and 11953 to trunk
barras
2009-03-02
*
Heavy modifications on the widget and edition tab creation mechanism.
vgross
2009-03-02
*
=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...
aspiwack
2009-02-27
*
extraction: update of README+CHANGES, rm of BUGS+TODO
letouzey
2009-02-27
*
Makefile: avoid building an empty contrib.cmxa
letouzey
2009-02-27
*
Amélioration de coq_makefile
notin
2009-02-24
*
Add support for dependent "destruct" over terms in dependent types.
herbelin
2009-02-23
*
CoqInterface.vo in CONTRIBVO (should fix a dependency issue)
letouzey
2009-02-20
*
On passe les last_mods (un des champs de Evd.evar_defs) de list
aspiwack
2009-02-20
*
On ne met plus rien dans les last_mods tant que conv_pbs est vide.
aspiwack
2009-02-20
*
coq-interface and coq-parser can be calls to coqtop with adequate code dynlink
letouzey
2009-02-20
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
maj de la faq: correction de l'exemple field qui compilait plus en 8.2, corre...
jnarboux
2009-02-17
*
#rectypes was already automatically added when using 3.11
herbelin
2009-02-17
*
Made hack to have Drop and #use"include" working with ocaml 3.10 public
herbelin
2009-02-17
*
report de r11926: install de coqchk
barras
2009-02-16
*
Fix [apply_in] which short-circuited resolution of evars in a custom
msozeau
2009-02-16
*
Bug 2050, commit v8.2 11923-11924 ---> trunk
soubiran
2009-02-13
*
Backport of 11890 from branch v8.2 (compile tools with the best
herbelin
2009-02-11
*
Gestion des espaces dans les noms + guess_coqlib sous Windows
notin
2009-02-11
*
Nouvelle icône pour Coq
notin
2009-02-11
*
Fix d'un petit problème de chemin sous Windows
notin
2009-02-11
*
Fix de divers petits problèmes d'installation
notin
2009-02-11
*
Fix d'un problème lors de l'appel à coqtop avec un chemin relatif
notin
2009-02-11
*
Modification du style du manuel de référence
notin
2009-02-11
*
Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin
2009-02-11
*
A few fixes for bug #2032 (backport r11857)
glondu
2009-02-11
*
Add -coqtoolsbyteflags and -custom to ./configure...
glondu
2009-02-11
*
Document how FIND_VCS_CLAUSE has to be used
lmamane
2009-02-11
*
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
[next]