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
*
Suite commit 11539 sur notation Record dans (Co)Inductive (MAJ
herbelin
2008-11-05
*
Petit bug dans le commit précédent.
aspiwack
2008-11-05
*
Nouvelle syntaxe pour écrire des records (co)inductifs :
aspiwack
2008-11-05
*
Better extraction renaming phase (fix #1914 plus other non-reported bugs)
letouzey
2008-11-05
*
Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)
herbelin
2008-11-04
*
2 petites améliorations de coq_makefile (traitement des .ml4 + cibles géné...
notin
2008-11-04
*
Fix CAMLHLIB (due to r11358) (Closes: #1986)
glondu
2008-11-02
*
test-suite/ideal-features/{apply.v -> eapply_evar.v}
glondu
2008-11-02
*
Ajout d'une option -raw pour Coqdoc (sortie en texte brut)
notin
2008-10-31
*
allowed patternidents starting with an '_'
amahboub
2008-10-31
*
The lexer is changer to break former PATTERNIDENT into two tokens.
amahboub
2008-10-30
*
Document native "Declare ML Module"
glondu
2008-10-29
*
Remove calls to Dynlink.add_{interfaces,available_units} altogether
glondu
2008-10-29
*
Adaptation du vieil appel à "apply" sur lemme de symétrie au cas où
herbelin
2008-10-29
*
Oups...
notin
2008-10-29
*
Dépendance des cibles de la documentation envers les cibles de Coq
notin
2008-10-29
*
Native "Declare ML Module" when possible
glondu
2008-10-28
*
petite modif du commit 11513.
soubiran
2008-10-28
*
11511 continued (bug in set.out + incohérence dans "Theorem with"
herbelin
2008-10-28
*
Correction bug 1979.
soubiran
2008-10-28
*
- Fixed many "Theorem with" bugs.
herbelin
2008-10-27
*
Correct enormous bug in interpretation of generalized binders: it simply
msozeau
2008-10-26
*
Fixes and refinements regarding occurrence selection:
herbelin
2008-10-26
*
adding an option Function_raw_tcc to Function
jforest
2008-10-26
*
Stop using a coqdocdoc env which prevents use of environments inside
msozeau
2008-10-26
*
- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)
herbelin
2008-10-26
*
Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui
herbelin
2008-10-26
*
More debugging of handling of open constrs with typeclasses:
msozeau
2008-10-25
*
Fix for bug #1981, correct the mismatch between the meta types used in
msozeau
2008-10-25
*
Raise informative errors instead of Failures or anomalies in case a meta
msozeau
2008-10-24
*
Fix doc of apply in (see coq-club message 26 September 2008)
herbelin
2008-10-24
*
Forgot one file which had other local modifications...
msozeau
2008-10-23
*
Fix bug #1977 by allowing the [apply] variants to take an [open_constr]
msozeau
2008-10-23
*
Open notation for declaring record instances.
msozeau
2008-10-23
*
Generalized implementation of generalization.
msozeau
2008-10-23
*
Fix bugs #1975 and #1976.
msozeau
2008-10-22
*
Fix for bug #1973 provided by Brian Campbell.
msozeau
2008-10-22
*
Various coqdoc improvements:
msozeau
2008-10-22
*
A much better implementation of implicit generalization:
msozeau
2008-10-22
*
Affichage des notations récursives:
herbelin
2008-10-22
*
More OCaml-3.11-friendly configure script
glondu
2008-10-21
*
warning message when a qualid to extract can be both a module or a cst
letouzey
2008-10-21
*
duplicated open of Ppconstr
letouzey
2008-10-21
*
Correction bug #1969.
soubiran
2008-10-21
*
Renommage "Global Instance" en "Instance Global" pour uniformisation
herbelin
2008-10-20
*
Zdiv: eqm (equality modulo some N) can now be declared as Parametric Relation
letouzey
2008-10-20
*
Syntaxe de COQBIN
notin
2008-10-20
*
Suite 11472 et 11473
herbelin
2008-10-19
*
Suite 11472
herbelin
2008-10-19
*
- Export de pattern_ident vers les ARGUMENT EXTEND and co.
herbelin
2008-10-19
[next]