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
*
New Arguments vernacular
gareuselesinge
2011-11-21
*
Adding the type infrastructure to handle properly API management of options
ppedrot
2011-11-18
*
Restore backward compatibility. ":>" declares subinstances in Class declarati...
msozeau
2011-11-18
*
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-17
*
Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...
aspiwack
2011-09-12
*
Break circular dependency Proof_global -> Vernacexpr -> Proof_global.
aspiwack
2011-05-17
*
New option [Set Bullet Behavior] allows to select the behaviour of bullets.
aspiwack
2011-05-13
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Add 'Existing Instances' declaration to declare multiple instances at once.
letouzey
2011-04-06
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
- Fix treatment of globality flag for typeclass instance hints (they
msozeau
2011-02-14
*
Annotations at functor applications:
letouzey
2011-02-11
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Add "Print Sorted Universes"
glondu
2011-01-11
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Fixing a bug introduced in r12304 (move of interpretation of
herbelin
2010-12-02
*
Remove Explain* vernacs
glondu
2010-10-06
*
Remove VernacGo
glondu
2010-10-06
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added command "Locate Ltac qid".
herbelin
2010-06-03
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Fail: a way to check that a command is refused without blocking a script
letouzey
2010-04-30
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Applying François Garillot's patch (#2261 in bug tracker) for extended
herbelin
2010-04-22
*
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
[next]