coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Clarification des contraintes sur le contexte de paramètres des	herbelin	2006-10-17
\| \| \| \| \| \| \| \| \| \| \|	inductifs dans le test de sous-typage (exigence du même nombre d'arguments uniformes attendus mais pas d'exigence spéciale sur les définitions locales du contexte à partir du moment où les types et constructeurs sont convertibles quand généralisés par rapport au contexte de paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9247 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Noms "canoniques" pour certaines des propriétés de xor.	herbelin	2006-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9246 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en forme des theories	notin	2006-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	affichage des ... dans les scripts	barras	2006-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typo doc + bug legacy field	barras	2006-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9243 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changes the use of lists and notations, to avoid that the notations	bertot	2006-10-16
\| \| \| \| \| \|	from BinList hide the 'List' type as soon as one requires a ring tactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9242 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification ocamldebug (coq-debug-programs.out obsolète)	herbelin	2006-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9241 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout des options Coqide suggérées par Damien Doligez (wish #1053)	notin	2006-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9240 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adaptation des tests suite à la modification de Rewrite .. in (r9201)	notin	2006-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9239 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction test-suite suite à r9186	notin	2006-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9238 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du théorème mult_minus_distr_l	notin	2006-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9237 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r9778@tannat: jforest \| 2006-10-13 11:36:37 +0200	jforest	2006-10-13
\| \| \| \| \| \| \|	Changement de nom des lemme de correction/completude des Functions vis a vis de leur graphes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9236 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection raise en début de séquence (en attendant que le code caché ↵	herbelin	2006-10-12
\| \| \| \| \| \|	trouve sa place) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9235 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix name clash on left	thery	2006-10-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9234 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de pages de man pour les exécutables coq	notin	2006-10-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9233 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une option -annotate au configure+ changement du comportement par ↵	notin	2006-10-11
\| \| \| \| \| \|	défaut de make git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9232 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix 0 obligations bug	msozeau	2006-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9231 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove duplicate conditions in Field + Monomial substitution function for PExpr	thery	2006-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9230 85f007b7-540e-0410-9357-904b9bb8a0f7
*	make sure BinList is not made visible to files that use the tactic Ring	bertot	2006-10-10
\| \| \| \| \| \| \|	because BinList contains an abbreviation to cons that makes printing of lists strange. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9229 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Exemple avec liaison des variables de filtrage du match	herbelin	2006-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9228 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration de l'automatisation des coupures quand deux idents se suivent	herbelin	2006-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9227 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Notations:	herbelin	2006-10-09
\| \| \| \| \| \| \| \| \| \| \| \|	- prise en compte des variables liées non liées par la notation (bug #1186), - test pour affichage des notations aussi sur les sous-ensembles des lieurs multiples (cf notation "#" dans output/Notations.v), - extension, correction et uniformisation de quelques fonctions sur les constr_expr et cases_pattern (avec incidences sur rawterm.ml, parsing et contrib/interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout combinateurs option_fold_left et name_fold_map	herbelin	2006-10-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9225 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite commit 9222 : rétablissement des tests autre que complexité	herbelin	2006-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9224 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement des nf_evar (source de complexité polynomiale) par de la	herbelin	2006-10-06
\| \| \| \| \| \| \| \| \| \| \| \|	réduction paresseuse. Accessoirement, suppression d'un test evar_defined inutile car sur résultat de whd_betadeltaiota qui contient la réduction evar de tête dans coercion.ml; code mort du commit précédent dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9223 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un répertoire de test de la complexité	herbelin	2006-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9222 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de on_judgment_type de Typeops vers Termops	herbelin	2006-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9221 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression d'une source de complexité polynomiale dans le pretypage	herbelin	2006-10-06
\| \| \| \| \| \| \| \| \|	(remplacement de la normalisation complète des evars dans les termes par une normalisation par nécessité - dans les types, c'est en général des expressions plus petites) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9220 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9219 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Annulation de l'essai de changement de sémantique du %scope (révision 9208).	herbelin	2006-10-06
\| \| \| \| \| \| \| \| \|	Retour à une sémantique où les %scope s'appliquent à la sous-expression complète (trop de pbs: constantes polymorphes sans arguments scope, variables locales de type fonctionnel, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9218 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ↵	notin	2006-10-05
\| \| \| \| \| \|	d'un constr c, on vérifie que c est clos dans l'environnement de m (#1183) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9217 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
\| \| \| \| \| \| \| \|	vis à vis de l'équivalence engendrées par les modules non génératifs (cf bug #1242) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9215 85f007b7-540e-0410-9357-904b9bb8a0f7
*	revert, the previous commit was a mistake	bertot	2006-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9214 85f007b7-540e-0410-9357-904b9bb8a0f7
*	avertissement a propos du commit 9211 dans CHANGES	letouzey	2006-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9213 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A version of natprering that should be more efficient and removal of a bad	bertot	2006-10-05
\| \| \| \| \| \|	comment in newring.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9212 85f007b7-540e-0410-9357-904b9bb8a0f7
*	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey	2006-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom	barras	2006-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9210 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrects the problem described in PR#1240:	bertot	2006-10-05
\| \| \| \| \| \| \| \|	if natprering modified the goal, then ring_simplify only performed the operation as natprering. Now, goals that are solved by ring should also be solved by (ring_simplify; reflexivity). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9209 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Essai de changement de sémantique du %scope :	herbelin	2006-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	1- ne s'applique plus que sur la notation immédiate au lieu de s'appliquer récursivement pour toutes les notations de l'expression concernée; 2- désactive la pile de scope pour cette notation immédiate. Le point 2 est clairement préférable pour les notations de la forme 3%sc, où on ne veut pas que 3 soit interprété dans un autre scope que sc même si sc n'a pas de notations numériques. Le point 1 est plus discutable et risque aussi de poser des incompatibilité (mais le comportement récursif peut être rétabli en changeant la valeur de quelques booléens marqués "recursive" dans constrextern.ml, constrintern.ml, et notation.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9208 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout String	herbelin	2006-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9207 85f007b7-540e-0410-9357-904b9bb8a0f7
*	inefficacite de field_simplify_eq	barras	2006-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9206 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1211	notin	2006-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9205 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1204 + maj CHANGES	notin	2006-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9204 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1236	notin	2006-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9203 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Doc injection as	herbelin	2006-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9202 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de comportement du [rewrite ... in H]: Coq échoue si H	notin	2006-10-03
\| \| \| \| \| \| \| \|	apparaît dans le but ou dans l'une des hypothèses (ferme les bugs #447, #883 et #1228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9201 85f007b7-540e-0410-9357-904b9bb8a0f7
*	le parsing du LETIN ne suivait pas la DTD (bug #1237)	herbelin	2006-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9200 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retour sur la suppression du pf_nf (trop d'exemples utilisent avec	herbelin	2006-10-03
\| \| \| \| \| \| \| \| \| \|	profit la simplification des arguments -- même si dans quelques cas trop de réduction obligent à revenir en arrière). Remplacement par un hack rapide (et non "scalable"). Suppression code mort oublié commit précédent sur equality.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9199 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ↵	herbelin	2006-10-03
\| \| \| \| \| \|	CSC) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9198 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveau ring/field	barras	2006-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9197 85f007b7-540e-0410-9357-904b9bb8a0f7