coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Syntaxe de COQBIN	notin	2008-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)	herbelin	2008-10-18
\| \| \| \| \| \| \| \| \|	- Makefile: typo apparente avec .ml4.preprocessed - test-suite: ajout d'un test sur eta qui trainait dans le coin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11465 85f007b7-540e-0410-9357-904b9bb8a0f7
*	## Lines starting with '## ' will be removed from the log message.	msozeau	2008-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	## File(s) to commit: ## tools/coqdoc/index.mll ## tools/coqdoc/output.ml ## tools/coqdoc/pretty.mll Various improvements to coqdoc: - (Hopefully) better handling of brackets and notations like \in (debugger with Stéphane Lescuyer). - More indexed tactics and commands. - Fix bug(?) in parsing of "[[" comments. - Better interpolation of module and library names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11432 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau	2008-10-03
\| \| \| \| \| \| \|	induction test-suite script. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11426 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Forgot one file.	msozeau	2008-09-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11422 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improvements in coqdoc:	msozeau	2008-09-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Better handling of spaces by actually ignoring what's inside proof scripts in light/gallina mode (detection of [Proof with] vs [Proof.] vs [Proof t.] and [Qed]/[Save]/...). - Provide fancy replacements for forall,/\,... etc in HTML in case the utf8 option is on. - Use typesetting information in HTML output and customize the CSS accordingly. The default color scheme follows closely the one set by Conor for Epigram; of course one can change it. - A try at interpolating identifiers in comments if they are defined in the same module, with a corresponding flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11421 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add types introduced by subtac in *.glob files	glondu	2008-09-15
\| \| \| \| \| \|	Hints from compilation warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1908 (améliorations de coqdoc.css)	notin	2008-09-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11361 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite 11266 (warning tools/gallina.ml)	herbelin	2008-07-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11267 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵	notin	2008-07-18
\| \| \| \| \| \|	de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage intempestif d'information de globalisation + numéro de version ↵	notin	2008-07-18
\| \| \| \| \| \|	dans coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11234 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- coqdoc: correction d'un bug sur les commentaires imbriqués	notin	2008-07-17
\| \| \| \| \| \| \| \|	- coq_makefile: amélioration des chemins de camlp4/5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11231 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oubli lors de la révision #11177	notin	2008-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11179 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵	notin	2008-06-25
\| \| \| \| \| \|	globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'option -dump-glob et ajout d'une option -no-glob	notin	2008-06-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Code cleanup in typeclasses, remove dead and duplicated code.	msozeau	2008-06-21
\| \| \| \| \| \| \|	Change from named_context to rel_context for class params and fields. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Little fixes: print unbound variable in error message (patch by Samuel	msozeau	2008-06-19
\| \| \| \| \| \| \| \|	Bronson), some keywords in coqdoc, and test well-typedness of predicate in subtac_cases after abstraction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11153 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin	2008-06-18
\| \| \| \| \| \| \| \|	(résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add possibility to match on defined hypotheses, using brackets to	msozeau	2008-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	disambiguate syntax: [ H := [ ?x ] : context C [ foo ] \|- _ ] is ok, as well as [ H := ?x : nat \|- _ ] or [H := foo \|- _ ], but [ H := ?x : context C [ foo ] ] will not parse. Add applicative contexts in tactics match, to be able to match arbitrary partial applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end will bind C to [ ∙ 1 2 ] and x to 0. Minor improvements in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un problème lié à une interaction entre hyperref et	notin	2008-06-12
\| \| \| \| \| \| \| \| \| \| \| \| \|	latex, qui empechait de produire des fichiers .dvi à partir des .tex générés par coqdoc. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/tools/coqdoc/coqdoc.sty M branches/v8.2/tools/coqdoc/coqdoc.sty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11120 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte de l'export des .cmi dans coq_makefile	notin	2008-06-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correct handling of DependentMorphism error, using tclFAIL instead of	msozeau	2008-06-10
\| \| \| \| \| \| \| \| \| \| \| \|	letting the exception go uncatched. - Reorder definitions in Morphisms, move the PER on (R ==> R') in Morphisms where it can be declared properly. Add an instance for Equivalence => Per. - Change bug#1604 test file to the new semantics of [setoid_rewrite at] - More unicode characters parsed by coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement des echo -e par printf + bug sur les exécutables ocaml dans ↵	notin	2008-06-09
\| \| \| \| \| \|	coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11079 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Enhancements to coqdoc, better globalization of sections and modules.	msozeau	2008-06-06
\| \| \| \| \| \| \| \|	Minor fix in Morphisms which prevented working with higher-order morphisms and PER relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11065 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix setoid_rewrite documentation examples.	msozeau	2008-06-03
\| \| \| \| \| \| \| \| \| \|	Debug handling of identifiers in coqdoc (should work with modules and sections) and add missing macros. Move theories/Program to THEORIESVO to put the files in the standard library documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improvements on coqdoc by adding more information into .glob	msozeau	2008-05-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex. Next step is to test and debug it on bigger developments. On the side: - Fix Program Let which was adding a Global definition. - Correct implicits for well-founded Program Fixpoints. - Add new [Method] declaration kind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add support for pdf in coqdoc, add export to pdf in coqide, port open and ↵	jnarboux	2008-05-28
\| \| \| \| \| \|	save as dialogs of coqide to a not deprecated widget, add filtering of *.v files in these dialogs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11006 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans coq_makefile: génération des règles implicites ↵	notin	2008-04-29
\| \| \| \| \| \|	en présence de l'option -custom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10869 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'options a coqdoc pour l'entete html	notin	2008-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10764 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction d'un bug de coq_makefile sur les variables CAMLLIBS et	notin	2008-04-03
\| \| \| \| \| \| \| \| \| \|	COQLIBS. - Ajout d'un message d'erreur si Camlp5 est compilé en mode strict git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10746 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug dans la gestion des dépendances vers les .ml	notin	2008-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et ↵	notin	2008-03-26
\| \| \| \| \| \|	coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10721 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des dépendances des .ml	notin	2008-03-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10719 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans la gestion des 'Declare ML Module'	notin	2008-03-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10717 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Various improvements of coqdep, resulting in a big speedup	letouzey	2008-03-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* use of Hashtbl for large sets/maps * reorganisation of directory-traversal functions, in order to avoid redundant stat / open * all files and directory whose names start by . are skipped while tranversing directories: no more visits of .svn ! * new option -boot to be used when computing dependencies of the stdlib: - no need in this case to records the system .vo in coqlibKnown - add directly inside coqdep the equivalent of -R theories Coq and -R contrib Coq As a result, coqdep'ing all the .vo of the stdlib now takes 25s on my machine instead of 2min30 earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10695 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New option -glob for coqdep, in order to avoid nasty tricks with sed in Makefile	letouzey	2008-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10668 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile : backtrack sur les liens vers les exécutables ocaml	notin	2008-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10638 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug de coq_makefile	notin	2008-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10633 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: correction de l'appel aux exécutables Ocaml	notin	2008-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10606 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: Correction d'un bug sur les options passées à Coqdoc	notin	2008-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Génération d'une toc en html et avec l'option -ps	notin	2008-02-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10597 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration de la gestion des chemins physiques (corrige au passage le bug ↵	notin	2008-02-27
\| \| \| \| \| \|	#939 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10594 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile: variables	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10586 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile: dépendances + génération des fichiers html	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10585 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug de coqdoc : les commentaires simples généraient des lignes vides	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10584 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug de Coqdoc (indentation des lignes)	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10583 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug de Coqdoc avec l'option -R	notin	2008-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10569 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reconnaissance des tokens dans les notations (suite à la revision r10562)	notin	2008-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10567 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1512	notin	2008-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10562 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'option -glob-from de Coqdoc: les globalisations sont	notin	2008-02-13
\| \| \| \| \| \| \| \|	lues directement des fichiers .glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10559 85f007b7-540e-0410-9357-904b9bb8a0f7