index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
CHANGES
Commit message (
Expand
)
Author
Age
*
Cleaned CHANGES (rough backport of 11855 from v8.2 to trunk).
herbelin
2009-01-27
*
- Structuring Numbers and fixing Setoid in stdlib's doc.
herbelin
2009-01-19
*
Added installation of .cmi files in "make install" target of coq_makefile.
herbelin
2009-01-04
*
Update
herbelin
2009-01-01
*
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
*
FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...
letouzey
2008-12-17
*
Extraction Blacklist : a new command for avoiding conflicts with existing files
letouzey
2008-12-16
*
About "apply in":
herbelin
2008-12-09
*
Minor improvement to commit 11619
herbelin
2008-11-23
*
Fixed bug #2006 (type constraint on Record was not taken into account) +
herbelin
2008-11-23
*
Fixed bug in VernacExtend printing + missing vernacular printing rules +
herbelin
2008-11-22
*
Nouvelle syntaxe pour écrire des records (co)inductifs :
aspiwack
2008-11-05
*
Document native "Declare ML Module"
glondu
2008-10-29
*
- Fixed many "Theorem with" bugs.
herbelin
2008-10-27
*
Renommage "Global Instance" en "Instance Global" pour uniformisation
herbelin
2008-10-20
*
- Export de pattern_ident vers les ARGUMENT EXTEND and co.
herbelin
2008-10-19
*
Backporting 11445 from 8.2 to trunk (negative conditions in
herbelin
2008-10-11
*
Add enough information to correctly globalize recursive calls in inductive and
msozeau
2008-09-11
*
Update CHANGES and INSTALL
glondu
2008-09-07
*
Renaming parser -> coq-parser
glondu
2008-08-18
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Add -browser option to configure script
glondu
2008-07-27
*
Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the
herbelin
2008-07-23
*
- Suppression de Rstar/Newman peu utilisables comme biblio (encodage
herbelin
2008-07-17
*
Quelques modifications autour du filtrage Ltac:
herbelin
2008-07-16
*
Documentation Prop<=Set et Arguments Scope Global
herbelin
2008-07-01
*
Lissage de la gestion des chemins de chargement de fichiers :
herbelin
2008-06-29
*
MAJ fichiers spécifiques trunk
herbelin
2008-06-22
*
Rename obligations_tactic to obligation_tactic and fix bugs #1893.
msozeau
2008-06-22
*
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2008-06-21
*
MAJ diverses
herbelin
2008-06-11
*
Documentation de "instantiate".
glondu
2008-06-09
*
- Documentation de admit et Print Assumptions.
herbelin
2008-06-09
*
- Patch sur "intros until 0"
herbelin
2008-06-08
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
add tiny change to coqide
jnarboux
2008-06-07
*
One (last?) more update of CHANGES.
letouzey
2008-06-05
*
more updates of CHANGES
letouzey
2008-06-04
*
Some updates of CHANGES (to be continued...)
letouzey
2008-06-03
*
Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in
letouzey
2008-06-01
*
- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"
herbelin
2008-05-30
*
update changes related to coqide
jnarboux
2008-05-27
*
- Nouvelle option "Set Printing Existential Instances" pour forcer
herbelin
2008-05-25
*
Ajout de la possibilité d'utiliser fix/cofix dans les notations.
herbelin
2008-05-24
*
refined the conversion oracle
barras
2008-05-21
*
Léger backtrack sur commit coqide précédent (si la commande à annuler
herbelin
2008-05-20
*
- Fix bug related to indices of fixpoints.
msozeau
2008-05-13
*
MAJ et bricoles diverses
herbelin
2008-05-12
[next]