coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Modifications de la construction de la documentation de la librairie	notin	2007-07-25
\| \| \| \| \| \| \| \| \| \| \| \| \|	standard: - ajout d'une entrée dans le Makefile principal pour le fichier de globalisations glob.dump - modifications de doc/Makefile et de l'index html pour gérer les nouveaux fichiers de la librairie standard (en part. ceux dans Ints) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10049 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n et	notin	2007-07-25
\| \| \| \| \| \| \| \|	do_norm. Corrigé par analogie avec N11, N12, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10048 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed bug 1448 and 1674	barras	2007-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10046 85f007b7-540e-0410-9357-904b9bb8a0f7
*	proof of compare added	thery	2007-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10045 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed bug 1675: computing carrier from the relation type was not right	barras	2007-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10043 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Declarative language: fixed the generation of fixpoints for induction proofs.	corbinea	2007-07-24
\| \| \| \| \| \| \| \|	Cleaner code: the guardedness bug is now corrected. Added "trivial" to the automation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An update on axiomatization of numbers.	emakarov	2007-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 85f007b7-540e-0410-9357-904b9bb8a0f7
*	removed thesis	barras	2007-07-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10040 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of Program and its tactics, fix enormous interaction bug due ↵	msozeau	2007-07-19
\| \| \| \| \| \|	to bad cache handling. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10032 85f007b7-540e-0410-9357-904b9bb8a0f7
*	some more svn:ignore properties	letouzey	2007-07-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10029 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A generic preprocessing tactic zify for (r)omega	letouzey	2007-07-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	------------------------------------------------ See file PreOmega for more details and/or test-suite/succes/Omega.v The zify tactic performs a Z-ification of your current goal, transforming parts of type nat, N, positive, taking advantage of many equivalences of operations, and of the positivity implied by these types. Integration with omega and romega: (r)omega : the earlier tactics, 100% compatible (r)omega with * : full zify applied before the (r)omega run (r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z}, applies only specific parts of zify (btw "with Z" means take advantage of Zmax, Zmin, Zabs and Zsgn). As a particular consequence, "romega with nat" should now be a close-to-perfect replacement for omega. Slightly more powerful, since (forall x:nat, x*x>=0) is provable and also slightly less powerful: if False is somewhere in the hypothesis, it doesn't use it. For the moment zify is done in a direct way in Ltac, using rewrite when necessary, but crucial chains of rewrite may be made reflexive some day. Even though zify is designed to help (r)omega, I think it might be of interest for other tactics (micromega ?). Feel free to complete zify if your favorite operation / type isn't handled yet. Side-effects: - additional results for ZArith, NArith, etc... - definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope - romega now start by doing "intros". Since the conclusion will be negated, and this operation will be justified by means of decidability, it helps to have as little as possible in the conclusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: slightly cleaner version of r10026	lmamane	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: don't mention bin/coqtop.byte twice to make when BEST=byte, it ↵	lmamane	2007-07-18
\| \| \| \| \| \|	complains. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10026 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleanly refuse to operate in the presence of unsaved changes in emacs	lmamane	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10025 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage de "thesis" seulement en mode déclaratif	herbelin	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10024 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oups... Use shell-variable syntax in shell commands.	lmamane	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10023 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: Revert r10015, which was based on a misunderstanding	lmamane	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Raffinement de interp_ident pour que l'ident interprété soit au choix	herbelin	2007-07-18
\| \| \| \| \| \| \| \|	frais (par exemple pour "intro") ou pas forcément (par exemple pour "fresh") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10021 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: needs GNU Make 3.81	lmamane	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10020 85f007b7-540e-0410-9357-904b9bb8a0f7
*	J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir	aspiwack	2007-07-18
\| \| \| \| \| \| \| \| \| \| \| \|	noté cette erreur de ma part (copier/coller mon amour). Ça créait des soucis dans les dépendance dans l'ancienne architecture de Makefile, probablement dans la nouvelle aussi dans certaines circonstances. Exit les bêtise, c'est plus propre maintenant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10019 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: more robustness all around	lmamane	2007-07-18
\| \| \| \| \| \| \| \|	- Make sure make notices when a command fails - don't leave behind half-baked output files of commands that failed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10016 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: Do _not_ delete dummy .ml files of .ml4 files even when not needed ↵	lmamane	2007-07-17
\| \| \| \| \| \|	anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10015 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Do not try to clean the doc when no config/Makefile	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10013 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reorganise cleaning targets	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10012 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: -MG doesn't (and can't) do what is necessary	lmamane	2007-07-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The -MG option causes gcc to add any non-found .h file verbatim in the dependencies. This naturally doesn't include the path to it (because the path is unknown) and thus make doesn't know how to build it; it knows how to build kernel/byterun/coq_jumptbl.h, not "coq_jumptbl.h". --This line, and those below, will be ignored-- M Makefile.common M Makefile.build git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10011 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A cleaner solution to "make deletes .ml4.d files -> infinite loop" problem	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oups... empty .ml4.d files produced	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CAMLP4DEPS will not work for .byteml and .optml	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10008 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Generalized CAMLP4USE for pp dependencies	corbinea	2007-07-16
\| \| \| \| \| \| \| \|	Removed parsing/lexer.ml4 special case No file depends on pa_extend_m.cmo anymore, Wierd ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: work around gcc bug: lhs of make rule created by -MM does not ↵	lmamane	2007-07-16
\| \| \| \| \| \|	include path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10006 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: in C, .d files need to depend on the same as the .o file	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	makefile: dependencies of .c files: assume missing headers are generated files	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: use CFLAGS for dependency generation of .c files	lmamane	2007-07-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10003 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An update on axiomatization of number classes.	emakarov	2007-07-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10002 85f007b7-540e-0410-9357-904b9bb8a0f7
*	some more useless constant in const_omega	letouzey	2007-07-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10001 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Beginning of a reorganisation of the ml part for romega:	letouzey	2007-07-13
\| \| \| \| \| \| \| \| \|	- deletion of some dead code - grouping all stuff depending on Z in a nice module Int git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10000 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A emacs-specific comment to use makefile-mode on Makefile.*	letouzey	2007-07-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9999 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added Qpower_plus' and Zpower_Qpower	roconnor	2007-07-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9997 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Small cleanup	letouzey	2007-07-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9996 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans le	herbelin	2007-07-13
\| \| \| \| \| \| \| \|	répertoire Num. Suppression de ce dernier de l'archive courante. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9995 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deletion of some firstorder calls in FSetAVL:	letouzey	2007-07-13
\| \| \| \| \| \| \| \| \|	after commit 9983 of Bruno concerning kernel/closure.ml, a few firstorder were awfully slow. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9994 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New bootstrapping, improved, Makefile system	corbinea	2007-07-13
\| \| \| \| \| \| \|	Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
*	removing a warning at compilation time	jforest	2007-07-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9991 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proof for sub	thery	2007-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9990 85f007b7-540e-0410-9357-904b9bb8a0f7
*	(Port of r9984) Easier debugging:	glondu	2007-07-12
\| \| \| \| \| \| \| \| \|	* explicitation of some types * tags for grammar entries git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9989 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update (test-suite was not successful).	glondu	2007-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9988 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deletion of an obsolete file (euclidian division done in old syntax with ↵	letouzey	2007-07-12
\| \| \| \| \| \|	realizers) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9987 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deletion of contrib/extraction/test	letouzey	2007-07-12
\| \| \| \| \| \| \| \| \| \|	Not maintained, probably broken, of no interest except (maybe) for myself, bad interaction with tools that work recursively (coqdep). ===> I move it to a personal repository git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9986 85f007b7-540e-0410-9357-904b9bb8a0f7
*	normalisation (by closure) was not performed under fixpoints	barras	2007-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9983 85f007b7-540e-0410-9357-904b9bb8a0f7
*	port de r9968: bug avec les ring calculatoires	barras	2007-07-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9982 85f007b7-540e-0410-9357-904b9bb8a0f7