coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Exploitation du 'let rec' + présentation	herbelin	2006-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8134 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New files for subtac	coq	2006-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8133 85f007b7-540e-0410-9357-904b9bb8a0f7
*	tactic haRVey pour appeler haRVey (contrib/dp)	filliatr	2006-03-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8110 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #842 (rename d'une hyp du contexte)	herbelin	2006-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8107 85f007b7-540e-0410-9357-904b9bb8a0f7
*	appel de Zenon	filliatr	2006-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	filliatr	2006-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8103 85f007b7-540e-0410-9357-904b9bb8a0f7
*	dp: sortie Why	filliatr	2006-02-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Work on recursive definitions	coq	2006-02-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8080 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add vernacular file for subtac	coq	2006-02-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8079 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Julien:	bertot	2006-02-22
\| \| \| \| \| \| \| \|	+ Induction principle for general recursion + Bug correction in structural principles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8076 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Work with binder lists, problem of tycons	coq	2006-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8073 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Latest fixes, should work fine now for non recursive definitions, although ↵	coq	2006-02-21
\| \| \| \| \| \|	still has some syntax problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8072 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix minor bug	coq	2006-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8069 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Forgot a file	coq	2006-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8068 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Monday work, working with coercions and implicit args	coq	2006-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8067 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Forgot another file...	coq	2006-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8066 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Forgot one file	coq	2006-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8065 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rewrite of the subtac tactic, needs some work on implicit arguments.	coq	2006-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8063 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug correction	bertot	2006-02-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8056 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Julien:	bertot	2006-02-17
\| \| \| \| \| \| \| \| \|	+ Compatibility with new induction + Induction principle for general recursion preparation still continuing + Cleaning dead code ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8055 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changed the decomposition of an induction scheme	coq	2006-02-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8052 85f007b7-540e-0410-9357-904b9bb8a0f7
*	firstorder fails gracefullly when encountering untypable higher-order terms	corbinea	2006-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8040 85f007b7-540e-0410-9357-904b9bb8a0f7
*	induction now admits multiple induction arguments. The principle must	coq	2006-02-10
\| \| \| \| \| \| \| \| \| \| \| \| \|	be explicitely given, and ALL parameters and args of the scheme must be given (only branches must be omitted). For the moment, only principle like generated by GenFixpoint (functional induction) are usable. That is the predicate must have a additional paramter like in: (P x1 ... xn (f p1...pm x1...xn)) Example of use : induction x y (add x y) using add_ind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8023 85f007b7-540e-0410-9357-904b9bb8a0f7
*	very minor bug correction and cleanning	bertot	2006-02-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8019 85f007b7-540e-0410-9357-904b9bb8a0f7
*	securing intros (we now use h_intro)	bertot	2006-02-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8018 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor bugs fixes	bertot	2006-02-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8017 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changing Set to Type for iter.	bertot	2006-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	One can use a measure {mes f x} instead of a well-founded relation in ↵	bertot	2006-02-08
\| \| \| \| \| \| \| \| \|	GenFixpoint. If the function takes only one argument, it can be deleted from the wf/mes part. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8013 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Julien:	bertot	2006-02-08
\| \| \| \| \| \| \| \| \|	+ Recursive definition (repository contrib/recdef) can now be used with GenFixpoint syntax by just replacing the usual {struct x} annotation by {wf R x} where x is one of the function declared arguments and R is a expression well-typed in the x typing environment. + Bug correction in new functional induction + For now no induction principle for general recursive definition is generated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8012 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added mli 's for the nex functional induction (forgotten last time).	coq	2006-02-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7980 85f007b7-540e-0410-9357-904b9bb8a0f7
*	+ Adding an error message when the function cannot be defined	bertot	2006-02-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7979 85f007b7-540e-0410-9357-904b9bb8a0f7
*	protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)	barras	2006-02-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)	barras	2006-02-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7973 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New version of functional induction / inversion. By Julien Forest,	coq	2006-02-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Benjamin Gregoire, Gilles Barthe. For the moment, it is as followed: If one uses GenFixpoint instead of Fixpoint, then induction principles are generated on the fly (respecting the match structure written by the user, with wildcards etc). These principles can be used directly or by tactics "new functional induction" and "functional inversion". We will soon make "new functional induction" become "functional induction", before release of V8.1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin	2006-01-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7937 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin	2006-01-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7936 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin	2006-01-24
\| \| \| \| \| \| \| \|	changé entre les version 3.08.4 et 3.09.0 (influe notamment sur l'ordre d'application des Hints de auto) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7925 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ↵	herbelin	2006-01-21
\| \| \| \| \| \|	et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7909 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et ↵	herbelin	2006-01-21
\| \| \| \| \| \|	fail peuvent maintenant être des listes de string, int et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7908 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Recursive Definition now supports functions with more than one argument.	coq	2006-01-18
\| \| \| \| \| \| \|	Julien git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7887 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin	2006-01-16
\| \| \| \| \| \| \| \|	choisir un nom; utilisation de IntroAnonymous au lieu de None dans l'argument "with_names" des tactiques induction, inversion et assert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7880 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin	2006-01-16
\| \| \| \| \| \| \| \|	- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns - TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changing well founded induction to fix on accessibility proof in order	bertot	2006-01-12
\| \| \| \| \| \| \| \|	to prepare the possibility to define function with more that one argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7856 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remove warnings that were left in the directory contrib/interface	bertot	2006-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7844 85f007b7-540e-0410-9357-904b9bb8a0f7
*	removes several warnings in contrib/interface	bertot	2006-01-11
\| \| \| \| \| \| \| \|	Modifies the behavior of Recursive definition to produce goals instead of established theorems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7843 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
\| \| \| \| \| \| \|	et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵	herbelin	2005-12-30
\| \| \| \| \| \|	de chaîne de caractères tel que "foo" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage coqlib	herbelin	2005-12-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7760 85f007b7-540e-0410-9357-904b9bb8a0f7
*	La distribution de Rocq/GRAPHS se fait via le serveur de contributions ↵	herbelin	2005-12-29
\| \| \| \| \| \|	utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7755 85f007b7-540e-0410-9357-904b9bb8a0f7