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
*
- Fixing declarative mode in presence of high use of Change_evars nodes
herbelin
2009-05-20
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
- Fixed a little bug in previous commit (bad failure in case of unknown entry).
herbelin
2009-04-27
*
- Cleaning (unification of ML names, removal of obsolete code,
herbelin
2009-04-27
*
- Fixing #2090 (occur check missing when trying to solve evar-evar equation).
herbelin
2009-04-25
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing
herbelin
2009-04-08
*
Avoid inadvertent declaration of "on" as a keyword. New syntax is
msozeau
2009-03-29
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
Parsing files for numerals (+ ascii/string) moved into plugins
letouzey
2009-03-27
*
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
[next]