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
*
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
*
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
*
- 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
*
Minor improvement to commit 11619
herbelin
2008-11-23
*
Fixed bug #2006 (type constraint on Record was not taken into account) +
herbelin
2008-11-23
*
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
*
Minor fixes related to coqdoc and --interpolate and the dependent
msozeau
2008-10-03
*
Add user syntax for creating hint databases [Create HintDb foo
msozeau
2008-09-14
*
In manual implicit arguments mode, do not enrich implicits
msozeau
2008-09-14
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Fixes in generalize_eqs/dependent induction to allow the user to specify
msozeau
2008-07-28
*
Suite commit 11236
notin
2008-07-24
*
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-07-22
*
Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...
notin
2008-07-18
*
Affichage intempestif d'information de globalisation + numéro de version dan...
notin
2008-07-18
*
fixed indentation of subgoals for Show Script
barras
2008-07-17
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Suite de la révision #11212
notin
2008-07-08
*
Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...
notin
2008-07-07
*
- Improve [Context] vernacular to allow arbitrary binders, not just
msozeau
2008-07-07
*
Lissage de la gestion des chemins de chargement de fichiers :
herbelin
2008-06-29
*
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...
notin
2008-06-25
*
Enhancements to coqdoc, better globalization of sections and modules.
msozeau
2008-06-06
*
Fix setoid_rewrite documentation examples.
msozeau
2008-06-03
*
Improvements on coqdoc by adding more information into .glob
msozeau
2008-05-30
*
- Nouvelle option "Set Printing Existential Instances" pour forcer
herbelin
2008-05-25
*
Strategy commands are now exported
barras
2008-05-22
[next]