coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixing bugs #2347 (part 2) and #2388: error message printing was done	herbelin	2010-09-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	too late, in a global environment which was no longer the correct one, leading to the failure of error printing (hence an anomaly) in case the command modified the state in several steps. Now, errors raised by vernac commands are processed in the same (intermediate) state they were raised from, just before rolling back to the original state. that modify the state in several Now, errors raised by vernac commands that modify the state in several steps (say S1, S2, ..., Sn) are processed in the state they were produced in (S1, S2, ... Sn-1), git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fail: a way to check that a command is refused without blocking a script	letouzey	2010-04-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	"Fail cmd" is similar to "Time cmd", but instead of printing the execution time, it reverse the exit status of cmd. "Fail cmd" is successful iff cmd has ended with an error. This was, we can demonstrate erroneous commands in a script for pedagogical or testing purpose without having to comment it in order to play the rest of the script in coqide/PG. Coq < Fail Foo. The command has indeed failed with message: => Error: Unknown command of the non proof-editing mode. Coq < Fail Check Prop. Prop : Type Error: The command has not failed ! Two more remarks: - Fail doesn't catch anomalies. - Yes it it possible to write things like Fail Fail ... :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12981 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delineating a API for Coq inside toplevel/vernac.ml	vgross	2010-02-12
\| \| \| \| \| \| \| \| \| \| \| \| \|	Coq use case are mostly thoses : - parsing a char stream to get a vernac expr - evaluating a vernac expr with backtracking - turning a knob with a vernac expr, no backtracking - loading an entire file - compiling an entire file - backtracking (no clean API for this yet) - peeking Coq state info (no clean API for this yet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12756 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
\| \| \| \| \| \| \| \| \|	- Clarification and documentation of the different styles of Local/Global modifiers in vernacexpr.ml - Addition of Global in sections for Open/Close Scope. - Addition of Local for Ltac when not in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Timeout message was not always displayed	barras	2009-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11960 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commande Timeout + compaction des traces de debug_tactic	barras	2009-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11959 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
\| \| \| \| \| \| \| \| \| \|	- Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing/improving management of uniform prefix Local and Global	herbelin	2009-01-14
\| \| \| \| \| \| \| \| \| \|	modifiers (added a "Syntax Checking" phase for raising a non interpretation error just after a dot is parsed -- maybe exaggerated complication for what we want to do ?). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin	2008-11-22
\| \| \| \| \| \| \| \| \| \|	revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Stop glob messages to be printed by default on stdout	letouzey	2008-07-23
\| \| \| \| \| \| \| \|	Jean-Marc, feel free to check I've not broken anything concerning coqdoc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11248 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
*	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
*	Added frozen state after each command.	courtieu	2008-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10836 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
\| \| \| \| \| \| \| \| \|	devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Une passe sur les warnings (ajout Options.warn déclenchée par ↵	herbelin	2007-02-24
\| \| \| \| \| \| \| \| \|	compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles + messages divers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning backtracking code, optimized "Backtrack n x y" when n is	courtieu	2006-12-28
\| \| \| \| \| \|	current state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de	herbelin	2006-11-21
\| \| \| \| \| \| \| \|	chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9398 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Indentation + svnprop	notin	2006-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9133 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réinitialisation de token_number à chaque compilation d'un nouveau fichier ↵	notin	2006-06-08
\| \| \| \| \| \|	(fixe le bug #914) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8924 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Autres suppressions de composantes du traducteur	herbelin	2005-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7744 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des ↵	herbelin	2005-12-26
\| \| \| \| \| \|	G_new en G_.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des Tactic Notation	herbelin	2005-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage et documentation de Library	herbelin	2005-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug 'Time Load foo'	herbelin	2004-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras	2004-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout entree pour exporter les debuts et fins de compilation en mode -xml	herbelin	2004-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5575 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modif des fixpoints pour que si on donne une notation au produit, les pts ↵	barras	2004-03-05
\| \| \| \| \| \|	fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
\| \| \| \| \| \| \| \|	dans le module de leur définition. Error_in_file dans Util et étendu avec possibilité de noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection table des locations lors de Load (pour coqdoc)	herbelin	2004-01-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5237 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5149 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug: faut brancher la sortie des tactiques sur stdout pendant traduction	herbelin	2003-11-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4940 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place traduction des tactiques apres evaluation pour permettre des ↵	herbelin	2003-11-09
\| \| \| \| \| \|	changements semantiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4839 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug traduction de auto.(simpl). en auto.simpl.	barras	2003-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4676 85f007b7-540e-0410-9357-904b9bb8a0f7
*	oups! ca compile maintenant	barras	2003-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4656 85f007b7-540e-0410-9357-904b9bb8a0f7
*	translator avoids printing a . followed by a ( by inserting a space	barras	2003-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4655 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pr_vernac est paresseux; States.unfreeze seulement après que msgnl ait	herbelin	2003-10-03
\| \| \| \| \| \| \|	dégelé pr_vernac; hack pour "Import nat_scope" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4524 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction aussi si -translate et -load-vernac-source	herbelin	2003-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4471 85f007b7-540e-0410-9357-904b9bb8a0f7
*	traducteur: affiche les commentaires a l'interieur des commandes	barras	2003-09-22
\| \| \| \| \| \| \|	extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plutôt que de faire "Load" silencieusement, en profiter pour traduire	herbelin	2003-09-18
\| \| \| \| \| \| \|	le fichier chargé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4410 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour cacher le contenu de Load au traducteur	herbelin	2003-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4403 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Debranchement du traducteur pour Load !	herbelin	2003-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4347 85f007b7-540e-0410-9357-904b9bb8a0f7