index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
usage.ml
Commit message (
Expand
)
Author
Age
*
Ensure that a function declared with a label is used with it
letouzey
2012-12-08
*
coqtop -time : display per-command timings
letouzey
2012-10-05
*
No more states/initial.coq, instead coqtop now requires Prelude.vo
letouzey
2012-08-23
*
Updating headers.
herbelin
2012-08-08
*
verbose compat notations : nicer option name
letouzey
2012-07-08
*
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2012-07-05
*
Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BIN
pboutill
2012-06-15
*
coq_makefile fixup
pboutill
2012-06-14
*
New step in purpose to get both camlp4 and camlp5 compatible coq_makefiles
pboutill
2012-06-12
*
lib directory is cut in 2 cma.
pboutill
2012-04-12
*
-user option removal
pboutill
2011-11-21
*
In Coq_config: get rid of coqsrc and make coqlib optional
glondu
2011-09-27
*
coqtop -config returns coq returns coq environments at exection time
pboutill
2011-04-28
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
Ide_slave: a more robust current_status () function
letouzey
2011-03-28
*
CoqIDE argv parsing delegated to coqtop
vgross
2010-09-14
*
Fix unescaped end-of-lines (OCaml warning 29)
glondu
2010-09-13
*
* By default, load proof terms.
regisgia
2010-08-31
*
* scripts/Coqc toplevel/Usage:
regisgia
2010-08-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Correct typo: -noglob takes no argument.
msozeau
2009-06-13
*
Fix de divers petits problèmes d'installation
notin
2009-02-11
*
Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin
2009-02-11
*
Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...
notin
2009-01-06
*
- Suppression date dans configure du trunk
herbelin
2008-12-26
*
Nettoyage des variables Coq et amélioration de coqmktop. Les
notin
2008-12-19
*
Tentative d'amélioration de la robustesse des Makefile générés par
notin
2008-11-13
*
Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...
notin
2008-07-18
*
Lissage de la gestion des chemins de chargement de fichiers :
herbelin
2008-06-29
*
Suppression de l'option -dump-glob et ajout d'une option -no-glob
notin
2008-06-24
*
Ajout d'une option -with-geoproof à la configuration et à l'exécution
notin
2006-06-09
*
MAJ options coqtop et coqc
herbelin
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Ajout nouvelles options
herbelin
2004-01-15
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
backtrack dans l'algo d'unification
barras
2002-04-10
*
raccourci -l en plus de -load-vernac-source
letouzey
2002-03-07
*
-dump-glob dans le usage
filliatr
2002-02-27
*
Ajout d'une option et d'une fonction compile pour fabriquer les .vo
herbelin
2001-09-18
*
*** empty log message ***
courant
2001-04-19
*
bug Print Proof; usage coqtop/coqc
filliatr
2001-04-06
*
option -verbose a coqc; option -i supprimée
filliatr
2001-03-21
*
entetes
filliatr
2001-03-15
*
Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...
herbelin
2000-12-06
*
- coqc: utilise le meilleur coq possible
filliatr
2000-11-24
*
retablissement de line_oriented_parser pour Yves
filliatr
2000-11-22
*
modules
filliatr
1999-12-12
[next]