index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernacentries.ml
Commit message (
Expand
)
Author
Age
*
Added new command "Set Parsing Explicit" for deactivating parsing (and
herbelin
2012-01-20
*
Arguments: check rename even if no implicit is specified
gareuselesinge
2011-12-19
*
Command Arguments: standardizing format of error messages and American spelling.
herbelin
2011-12-17
*
Moving bullets (-, +, *) into stand-alone commands instead of being
courtieu
2011-12-16
*
Proof using ...
gareuselesinge
2011-12-12
*
Minor fixes to Arguments
gareuselesinge
2011-12-06
*
Added a DEPRECATED flag in declaration of options. For now only two options a...
ppedrot
2011-11-24
*
Correct direction for definitional typeclasses
msozeau
2011-11-24
*
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
*
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
*
First attempt at making Print Assumption compatible with opaque modules (fix ...
letouzey
2011-10-25
*
Re-allowing assumptions during proofs seems safe now (fix #2411)
letouzey
2011-09-15
*
Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...
aspiwack
2011-09-12
*
Lib.node: merge OpenedModtype and OpenedModule, same for Closed...
letouzey
2011-09-05
*
Remove code concerning the obsolete Set/Unset Undo
letouzey
2011-09-05
*
Misc improvements concerning "Show Match" and its coqide equivalent
letouzey
2011-08-18
*
This option disables the use of the '{| field := ... |}' notation
herbelin
2011-07-16
*
New option [Set Bullet Behavior] allows to select the behaviour of bullets.
aspiwack
2011-05-13
*
Print Module (Type) M now tries to print more details
letouzey
2011-05-11
*
Fixed a bug causing inconsistent states during proof editting.
aspiwack
2011-04-29
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Fixed "Eval ... in t" when t has still metavariables.
herbelin
2011-04-08
*
Add 'Existing Instances' declaration to declare multiple instances at once.
letouzey
2011-04-06
*
Goptions: repair Unset for int options
letouzey
2011-03-17
*
Added a table for using reserved names for binding names to types
herbelin
2011-03-05
*
- Fix treatment of globality flag for typeclass instance hints (they
msozeau
2011-02-14
*
Annotations at functor applications:
letouzey
2011-02-11
*
Started to fix the declarative proof mode (C-zar).
aspiwack
2011-02-10
*
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
*
Use dashed lines for equivalence edges in dot output of universes
glondu
2011-01-11
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Add information of localisation when an error involving an "implicit
herbelin
2010-11-07
*
In Univ, unify order_request and constraint_type
glondu
2010-11-03
*
Output universe graph in DOT language if output file ends in .dot or .gv
glondu
2010-11-02
*
More generic Univ.dump_universes
glondu
2010-11-02
*
Add tolerance for existential variables in Check.
herbelin
2010-10-31
*
Remove Explain* vernacs
glondu
2010-10-06
*
Remove VernacGo
glondu
2010-10-06
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Making display of various informations about constants more modular:
herbelin
2010-10-03
*
Fix function applications without labels (OCaml warning 6)
glondu
2010-09-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 too
herbelin
2010-09-18
[next]