index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
...
*
Remove unused mli files
letouzey
2009-03-27
*
- Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"
herbelin
2009-03-23
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
*
Optionally list opaque constants in addition to axions/variables in
msozeau
2009-03-09
*
commande Timeout + compaction des traces de debug_tactic
barras
2009-03-04
*
Do not reserve the keyword "Infer".
puech
2009-02-03
*
Les records déclarés avec Record ne peuvent plus être récursifs (le
aspiwack
2009-01-19
*
- Structuring Numbers and fixing Setoid in stdlib's doc.
herbelin
2009-01-19
*
Getting rid of the previous implementation of setoid_rewrite which was
msozeau
2009-01-18
*
Last changes in type class syntax:
msozeau
2009-01-18
*
DISCLAIMER
puech
2009-01-17
*
Fixing #1960 (xml bug with external on goal variable) and #1961
herbelin
2009-01-14
*
Fixing/improving management of uniform prefix Local and Global
herbelin
2009-01-14
*
- Standardized prefix use of "Local"/"Global" modifiers as decided in
herbelin
2009-01-13
*
Fixing a cosmetic tactic printer bug in passing
herbelin
2009-01-07
*
- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",
herbelin
2009-01-02
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
- Another bug in get_sort_family_of (sort-polymorphism of constants and
herbelin
2008-12-28
*
- coq_makefile: target install now respects the original tree structure
herbelin
2008-12-24
*
Generalized binding syntax overhaul: only two new binders: `() and `{},
msozeau
2008-12-14
*
About "apply in":
herbelin
2008-12-09
*
closed bug 1898: fold x in x; added a reordering primitive tactic
barras
2008-11-26
*
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
*
Fix mixup between Record, Structure and Class by adding a new variant for
msozeau
2008-11-10
*
Oops... forgot to commit a file related to r11561.
msozeau
2008-11-09
*
More factorization of inductive/record and typeclasses: move class
msozeau
2008-11-09
*
- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in
herbelin
2008-11-09
*
Move Record desugaring to constrintern and add ability to use notations
msozeau
2008-11-05
*
Nouvelle syntaxe pour écrire des records (co)inductifs :
aspiwack
2008-11-05
*
allowed patternidents starting with an '_'
amahboub
2008-10-31
*
The lexer is changer to break former PATTERNIDENT into two tokens.
amahboub
2008-10-30
*
Fixes and refinements regarding occurrence selection:
herbelin
2008-10-26
*
Open notation for declaring record instances.
msozeau
2008-10-23
*
Generalized implementation of generalization.
msozeau
2008-10-23
*
A much better implementation of implicit generalization:
msozeau
2008-10-22
*
Affichage des notations récursives:
herbelin
2008-10-22
*
duplicated open of Ppconstr
letouzey
2008-10-21
*
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
*
Report des commits 11417 et 11437 de la v8.2
soubiran
2008-10-15
*
Backporting 11445 from 8.2 to trunk (negative conditions in
herbelin
2008-10-11
*
Add user syntax for creating hint databases [Create HintDb foo
msozeau
2008-09-14
*
Add the ability to declare [Hint Extern]'s with no pattern.
msozeau
2008-09-07
*
Fixes in typeclasses resolution. Avoid reducing instances types before
msozeau
2008-09-07
*
Better handling of the opacity of proof obligations, add the possibility of
msozeau
2008-09-07
*
Report 11364 de 8.2 vers trunk (bugs affichage Print Module)
herbelin
2008-09-05
*
Correct handling of implicit arguments in [Equations] definitions,
msozeau
2008-09-03
[prev]
[next]