coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin	2008-02-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	maintenant écrire des fonctions récursives qui n'ont pas l'apparence d'être fonctionnelle. La sémantique reste toutefois différente. Par exemple, dans Ltac is := let rec i := match goal with \|- ?A -> ?B => intro; i \| _ => idtac end in i. l'évaluation de i est paresseuse, alors que dans une version non récursive Ltac is := let i := match goal with \|- ?A -> ?B => intro \| _ => idtac end in i. l'évaluation de i est forte (et échoue sur le "match" qui n'est pas autorisé à retourner une tactique). (note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10495 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Debug implementation of dependent induction/dependent destruction and ↵	msozeau	2008-01-31
\| \| \| \| \| \|	document it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finish let\| implementation and document it	msozeau	2008-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10489 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added full documentation for mathematical mode (draft version)	corbinea	2008-01-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10479 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous Coqide	notin	2008-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a note about the ambiguity of the syntax "qualid" in "tacarg"	herbelin	2008-01-05
\| \| \| \| \| \| \| \|	(see coq-club message from 3 Jan 2008). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10422 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation du format des références croisées vers Figure, Section, ↵	herbelin	2008-01-05
\| \| \| \| \| \| \| \| \| \| \|	Chapter Remplacement pageref par ref parce que pageref n'a pas de sens pour la version HTML git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10421 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Maj du lien vers coq-bugs dans Coqide.	glondu	2007-12-18
\| \| \| \| \| \| \|	On devrait mettre une redirection a l'ancienne adresse... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10390 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de la question no 172 de la FAQ (cf bug #1755)	notin	2007-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10363 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de l'axiomatisation des entiers à la documentation de la librairie ↵	notin	2007-11-28
\| \| \| \| \| \|	standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10343 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Doc update	msozeau	2007-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10258 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added the doc for the new Scheme Equality command	vsiles	2007-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10225 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation of commit 10188	letouzey	2007-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10198 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin	2007-10-03
\| \| \| \| \| \| \| \|	Mise à jour du tableau des axiomes dans la FAQ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10170 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix a problem doing 'make clean' under Winodws	notin	2007-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10165 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changes in Backtrack documentation. More accurate.	courtieu	2007-09-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10141 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added the documentation for Backtrack and BackTo.	courtieu	2007-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10139 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Indication de quel type de constantes est dépliable dans "simpl" (cf	herbelin	2007-09-19
\| \| \| \| \| \| \| \| \|	message de Benjamin Pierce de sep 2007 sur coq-club) [report de la révision 10128 de la 8.1 vers le trunk] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10129 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ date copyright doc	herbelin	2007-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10127 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A word on the measure and wf modifiers	msozeau	2007-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10110 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server	herbelin	2007-08-30
\| \| \| \| \| \| \| \| \|	et Set Whelp Getter pour changer le nom des serveurs (report 10105 de la 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add info on measure based defs.	msozeau	2007-08-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10095 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Save IS NOT the same Defined ....	msozeau	2007-08-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10084 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Erreur de copier/coller dans la section Guarded	notin	2007-08-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10079 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1635	notin	2007-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10073 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de control_only_guard, qui utilise maintenant	notin	2007-08-09
\| \| \| \| \| \| \| \| \| \| \| \|	iter_constr_with_full_binders + documentation de Guarded. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/doc/refman/RefMan-pro.tex M trunk/pretyping/inductiveops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10065 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A better Program documentation. Include it in the generated stdlib doc.	msozeau	2007-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Move Program tactics into a proper theories/ directory as they are general ↵	msozeau	2007-08-07
\| \| \| \| \| \|	purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrected the reference to glob.dump, which is used to create ↵	emakarov	2007-07-26
\| \| \| \| \| \|	stdlib/index-body.html. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10051 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	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
*	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
*	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
*	More natural notation for intro pattern: @a -> ?a	glondu	2007-07-09
\| \| \| \| \| \| \| \| \| \| \|	Caveat about a slight loss of compatibility: Some intro patterns don't need space between them. In particular intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it is still legal but equivalent to intros ?a ?b. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9964 85f007b7-540e-0410-9357-904b9bb8a0f7
*	If a fixpoint is not written with an explicit { struct ... }, then	letouzey	2007-07-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. When the system accepts a fixpoint, it now prints which decreasing argument was used, e.g: plus is recursively defined (decreasing on 1st argument) The search is quite brute-force, and may need to be optimized for huge mutual fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback. N.B. in the standard library, only 4 functions have an decreasing argument different from the one that would be automatically infered: List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind And compiling with as few explicit struct as possible would add about 15s in compilation time for the whole standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding a syntax for "n-ary" rewrite:	letouzey	2007-07-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	rewrite H, H' means: rewrite H; rewrite H'. This should still be compatible with other "features" of rewrite: like orientation, implicit arguments (t:=...), and "in" clause. Concerning the "in" clause, for the moment only one is allowed at the very end of the tactic, and it applies to all the different rewrites that are done. For instance, if someone _really_ wants to use all features at the same time: rewrite H1 with (t:=u), <-H2, H3 in * means: rewrite H1 with (t:=u) in ; rewrite <- H2 in ; rewrite H3 in * git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7
*	extension of the rename tactic: the following is now allowed:	letouzey	2007-07-06
\| \| \| \| \| \| \| \|	rename A into B, C into D, E into F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9952 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New intro pattern "@A", which generates a fresh name based on A.	glondu	2007-07-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9950 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C))	letouzey	2007-07-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9949 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation of f_equal and revert and case_eq (and ↵	letouzey	2007-07-05
\| \| \| \| \| \|	s/lri.fr/pps.jussieu.fr/ in my bib entry) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9944 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typo faq	herbelin	2007-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9895 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov	2007-06-08
\| \| \| \| \| \| \|	Added a tactic "now" which is nonrecursive but generalizes "trivial". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9884 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout doc clear sans argument	herbelin	2007-06-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9880 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug #1540 (typo on name .coqide-gtk2rc)	herbelin	2007-05-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9828 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- MAJ entêtes des fichiers produits par coq_makefile	herbelin	2007-05-16
\| \| \| \| \| \| \| \|	- Correction de bugs dans la reconnaissance d'un "*)" potentiel dans les lignes correspondant au mécanisme "section" de coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Made some places in the reference manual clearer. Corrected	emakarov	2007-05-11
\| \| \| \| \| \| \|	an example about modules that produced a Coq error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9820 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout possibilité d'options à trois mots.	herbelin	2007-04-29
\| \| \| \| \| \| \| \| \| \|	Suppression au passage syntaxe "Set table field ref", synonyme de "Add table field ref" et de "Unset table field ref", synonyme de "Remove table field ref". Changement de la syntaxe "Test tabel field val" en ""Test tabel field for val". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation de Existential et de Show Existential (fixes bug #1294)	notin	2007-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9799 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed some typos.	glondu	2007-04-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9789 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrected a LaTeX typo.	emakarov	2007-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9784 85f007b7-540e-0410-9357-904b9bb8a0f7