coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	oups, ne chargeait pas les bons fichiers	letouzey	2006-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9278 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin	2006-10-25
\| \| \| \| \| \| \| \|	du rôle de l'argument (-1) de make_clenv_binding_apply; nouvelle correction qui évite ce codage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9277 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqdep -slash	barras	2006-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9276 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ménage	notin	2006-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9275 85f007b7-540e-0410-9357-904b9bb8a0f7
*	oops	barras	2006-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9274 85f007b7-540e-0410-9357-904b9bb8a0f7
*	conflit de nom (Field_theory) modulo la casse	barras	2006-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9273 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de fresh (suite)	herbelin	2006-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9272 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de la valeur par défaut de with_geoproof (stabilité coqide)	notin	2006-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test apply in	herbelin	2006-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9270 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Insère une coercion vers Sortclass dans 'contradiction' si nécessaire	herbelin	2006-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9269 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de la tactique 'remember'	herbelin	2006-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9268 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de la primitive ltac fresh pour qu'elle accepte une liste de	herbelin	2006-10-24
\| \| \| \| \| \| \|	noms et de chaînes qu'elle va concaténer pour créer un nom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9267 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de la tactique "apply in".	herbelin	2006-10-24
\| \| \| \| \| \| \|	Au passage, déplacement des tactiques cut and co plus en amont + commentaires. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9266 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hack peu élégant pour permettre de parser des listes avec séparateurs dans	herbelin	2006-10-24
\| \| \| \| \| \| \|	TACTIC EXTEND git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9265 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Interprétation du terme comme type dans 'change' si pas de 'with' (pour ↵	herbelin	2006-10-24
\| \| \| \| \| \|	bénéficier des coercions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9264 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed same_file (#1141)	barras	2006-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9263 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed non-bug #1213	barras	2006-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9262 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug #1194: normalisation evars a la sortie de focus	barras	2006-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9261 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed "Show intros" which did not look at hypothesis.	courtieu	2006-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9260 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add a flush after backtracking x y z and before printing subgoals.	courtieu	2006-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9259 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add a flush for a warning.	courtieu	2006-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9258 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin	2006-10-21
\| \| \| \| \| \| \| \|	(avec comme conséquence des échecs en cas de beta-redex - cf coercions.v). Allègements triviaux dans coercion.ml en passant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9257 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pas d'@ dans les identificateurs (pour F4 and co)	herbelin	2006-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9256 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin	2006-10-21
\| \| \| \| \| \| \|	de subst1 au lieu de subst_term). Indentation plus compacte au passage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9255 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9254 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1255 (réécriture setoid sous un produit)	notin	2006-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9253 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de la localisation des erreurs en interactif (numéro de	herbelin	2006-10-20
\| \| \| \| \| \| \| \|	ligne relatif à la ligne au lieu de absolu par rapport à la session) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9252 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Starting to add a function schemes merging command (not finished, not	courtieu	2006-10-20
\| \| \| \| \| \| \|	activated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9251 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction sym -> comm	herbelin	2006-10-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9250 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: affichage des sous-buts et hypothèses et métas comme types de	herbelin	2006-10-19
\| \| \| \| \| \| \| \| \|	telle sorte que les coercions vers sortclass ne soient pas affichées (comme dans coqtop) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9249 85f007b7-540e-0410-9357-904b9bb8a0f7
*	field_simplify_eq profite de la factorisation de Laurent	barras	2006-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9248 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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