index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernacexpr.ml
Commit message (
Expand
)
Author
Age
*
Several bug-fixes and improvements of coqdoc
herbelin
2010-03-29
*
Fixes in rewrite and a Elimination/Case to Scheme:
msozeau
2010-03-06
*
New command Declare Reduction <id> := <conv_expr>.
letouzey
2010-01-28
*
Variant !F M for functor application that does not honor the Inline declarations
letouzey
2010-01-17
*
Include can accept both Module and Module Type
letouzey
2010-01-07
*
Specific syntax for Instances in Module Type: Declare Instance
letouzey
2010-01-04
*
Fix "Existing Instance" to handle globality information and "Existing
msozeau
2009-12-27
*
Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...
letouzey
2009-12-08
*
No more specific syntax "Include Self" for inclusion of partially-applied fun...
letouzey
2009-12-07
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
Module subtyping : allow many <: and module type declaration with <:
letouzey
2009-11-18
*
New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))
letouzey
2009-11-16
*
Include Self (Type) Foo: applying a (Type) Functor to the current context
letouzey
2009-11-16
*
Added support for multiple where-clauses in Inductive and co (see wish #2163).
herbelin
2009-11-11
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Add a new vernacular command for controling implicit generalization of
msozeau
2009-10-27
*
Documentation of the Local and Global modifiers.
herbelin
2009-10-27
*
New cleaning phase of the Local/Global option management
herbelin
2009-10-26
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
*
Add support for Local Declare ML Module
glondu
2009-09-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-11
*
Stop unnecessary use of lazy values for constraints, simplifying
msozeau
2009-09-02
*
Ajout de la gestion de Local et Global pour les options (au sens de
aspiwack
2009-08-14
*
Add support for "Infix ... := constr" instead of just "Infix ... := ref".
herbelin
2009-08-11
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
- Cleaning (unification of ML names, removal of obsolete code,
herbelin
2009-04-27
*
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
*
Les records déclarés avec Record ne peuvent plus être récursifs (le
aspiwack
2009-01-19
*
Getting rid of the previous implementation of setoid_rewrite which was
msozeau
2009-01-18
*
DISCLAIMER
puech
2009-01-17
*
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
*
- 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
*
Generalized binding syntax overhaul: only two new binders: `() and `{},
msozeau
2008-12-14
*
Fix mixup between Record, Structure and Class by adding a new variant for
msozeau
2008-11-10
*
More factorization of inductive/record and typeclasses: move class
msozeau
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
*
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
*
- New auto hints for transparency/opacity control, not bound to
msozeau
2008-08-22
*
- Improve [Context] vernacular to allow arbitrary binders, not just
msozeau
2008-07-07
*
Fixes in handling of implicit arguments:
msozeau
2008-07-04
*
Improvements on coqdoc by adding more information into .glob
msozeau
2008-05-30
[next]