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
...
*
Fix unescaped end-of-lines (OCaml warning 29)
glondu
2010-09-13
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Some fine-tuning after removal of automatic imports of coercions in r13310
herbelin
2010-07-23
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
Constrintern: unified push_name_env and push_loc_name_env; made
herbelin
2010-07-22
*
Added command "Locate Ltac qid".
herbelin
2010-06-03
*
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
*
Small improvements around coqdoc (including fix for bug #2288)
herbelin
2010-03-30
*
Several bug-fixes and improvements of coqdoc
herbelin
2010-03-29
*
New command Declare Reduction <id> := <conv_expr>.
letouzey
2010-01-28
*
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
*
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
*
Now "Include Self <expr>" handles partially applied functors, cf for example ...
soubiran
2009-11-18
*
Allow interactive proofs in module types
letouzey
2009-11-18
*
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
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
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
*
New cleaning phase of the Local/Global option management
herbelin
2009-10-26
*
Fix bug #2162 and a name clashing bug in generalized binders.
msozeau
2009-10-09
*
Add support for Local Declare ML Module
glondu
2009-09-29
*
Add the option to automatically introduce variables declared before the
msozeau
2009-09-22
*
Replace call to where_in_path by find_file_in_path in "Locate File"
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Backtrack on the forced discharge of type class variables introduced
msozeau
2009-09-14
*
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-11
*
Postpone checking of Local/Global to allow grammar extensions to use it
msozeau
2009-09-02
*
Ajout de la gestion de Local et Global pour les options (au sens de
aspiwack
2009-08-14
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Fix implicit args code so that declarations are added for all
msozeau
2009-05-27
*
Stop using a "Manual Implicit Arguments" flag and support them as soon
msozeau
2009-05-27
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
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
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
*
Getting rid of the previous implementation of setoid_rewrite which was
msozeau
2009-01-18
*
DISCLAIMER
puech
2009-01-17
[prev]
[next]