coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	args implicites dans Field	barras	2006-09-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9192 85f007b7-540e-0410-9357-904b9bb8a0f7
*	separation de RealField	barras	2006-09-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commit de field + renommages	barras	2006-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin	2006-09-22
\| \| \| \| \| \| \| \|	Tactic Notation acceptant des listes en entrée avec application à la définition de revert dans Tactics.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9159 85f007b7-540e-0410-9357-904b9bb8a0f7
*	incomplete and temporary fix for PR#1222: revert accepts up to 10 args	letouzey	2006-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9156 85f007b7-540e-0410-9357-904b9bb8a0f7
*	better scope/require managment (patch by Russel O'Connor)	letouzey	2006-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9155 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Indentation + typo	notin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à une définition de inhabited plus dans les 'standard ↵	herbelin	2006-08-28
\| \| \| \| \| \|	mathématiques'; ajout preuve que tous les 'epsilon i P' sont égaux si P habité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9093 85f007b7-540e-0410-9357-904b9bb8a0f7
*	"Essai de remplacement de "ex P" par "exists x, P x" suite à	herbelin	2006-08-28
\| \| \| \| \| \| \| \|	l'introduction d'unification de motifs à la Miller permettant une forme restreinte canonique d'unification du second ordre git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	JMeq maintenant applicable sur Type	herbelin	2006-08-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9077 85f007b7-540e-0410-9357-904b9bb8a0f7
*	comparison functions should be Defined not Qed	letouzey	2006-08-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9066 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage sqtr_lem_1 (bug 1189)	notin	2006-07-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9052 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de quelques Arguments Scope pour simuler la récursivité du scope ↵	herbelin	2006-07-11
\| \| \| \| \| \|	Rfun_scope en compensation (et anticipation) d'une suppression de la récursivité des délimiteurs de scope (ici %F) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9042 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Argument Scope de list déplacé dans List.v	herbelin	2006-07-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9035 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2006-07-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9026 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques Hint inutiles	herbelin	2006-07-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9025 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ du manuel de référence	notin	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8999 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de Zgcd_spec (compat.)	notin	2006-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8990 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey	2006-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8989 85f007b7-540e-0410-9357-904b9bb8a0f7
*	repetition d'hypotheses dans well_founded_induction_type_2	letouzey	2006-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8988 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage des graphes de Function dans Type	jforest	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification déf de exists! pour éviter une éta-expansion et pouvoir ↵	herbelin	2006-06-09
\| \| \| \| \| \|	être filtré facilement par 'ex (unique ?P)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8936 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement Int.v dans ZArith, déplacement de DecidableType.v et ↵	herbelin	2006-06-09
\| \| \| \| \| \|	DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 85f007b7-540e-0410-9357-904b9bb8a0f7
*	+ ameliorating the tactic "functional induction"	jforest	2006-06-06
\| \| \| \| \| \| \| \|	+ bug correction in proof of structural principles + up do to date test-suite/success/Funind.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome ↵	letouzey	2006-06-05
\| \| \| \| \| \|	d'extensionalite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8897 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict ↵	herbelin	2006-06-04
\| \| \| \| \| \|	with FSets git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8894 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout exists! et restructuration/extension des fichiers sur la	herbelin	2006-06-04
\| \| \| \| \| \| \|	description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8893 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout exists! et restructuration/extension des fichiers sur la	herbelin	2006-06-04
\| \| \| \| \| \| \|	description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8892 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout de QArith dans les theories standards	letouzey	2006-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8883 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petits ajouts	letouzey	2006-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8882 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Replacing the old version of "functional induction" with the new one.	jforest	2006-05-31
\| \| \| \| \| \| \|	The old version is, for now, still available by prefixing any command/tactic with Old/old (eg. old functional induction ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8881 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* suite de la revision des wrappers Make	letouzey	2006-05-30
\| \| \| \| \| \| \|	* quelques unfold E.eq en cas de changement de la semantique des foncteurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8876 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'alias pour prodT_rect et cie qui avaient Ã©tÃ© oublkÃiÃ©s	herbelin	2006-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8872 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
\| \| \| \| \| \| \| \| \| \| \|	sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite changement précédence by de assert	herbelin	2006-05-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de prÃ©cÃ©dence de l'argument du by de assert; ↵	herbelin	2006-05-23
\| \| \| \| \| \|	consÃ©quences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un debut de propriétés concernant FMap	letouzey	2006-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8844 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite des marquages de types et opacifications de lemmes dans les wrappers Make	letouzey	2006-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8843 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ↵	herbelin	2006-05-22
\| \| \| \| \| \|	bas, i.e. Set; renommage canonique Rmax_comm git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8838 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ↵	herbelin	2006-05-22
\| \| \| \| \| \|	bas, i.e. Set; renommage canonique Rmax_comm git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8837 85f007b7-540e-0410-9357-904b9bb8a0f7
*	auto with zarith genere des sous-lemmes silencieusement,	letouzey	2006-05-20
\| \| \| \| \| \| \| \|	et ... <: ... with E:=Z_as_OT n'aime pas ca git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8836 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite tentative pour permettre l'utilisation de modules de FSets	letouzey	2006-05-20
\| \| \| \| \| \| \| \| \|	avec <: au lieu de : sans surprise de modules genre Raw partout ou autres alias dépliés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8834 85f007b7-540e-0410-9357-904b9bb8a0f7
*	on cache autant que possible Raw dans FSet(Weak)List.Make	letouzey	2006-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8833 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 ↵	letouzey	2006-05-18
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo dans List.v	notin	2006-05-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de [count_occ] dans List.v	notin	2006-05-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8824 85f007b7-540e-0410-9357-904b9bb8a0f7
*	etoffage des notions de permutations (a la fois List.Permutation et ↵	letouzey	2006-05-16
\| \| \| \| \| \|	Permutation.permutation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	3*rien	letouzey	2006-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8820 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout d'exemples de decidable types	letouzey	2006-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8819 85f007b7-540e-0410-9357-904b9bb8a0f7