coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Réajout de eq_rec_eq oublié lors de la modularisation de Eqdep	herbelin	2006-03-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8674 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Inductifs avec polymorphisme de sorte (version initiale)	herbelin	2006-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout array_fold_map', list_fold_map' et list_remove_first	herbelin	2006-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8672 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pour coqdoc	letouzey	2006-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8671 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nommage explicite de certains "intro" pour préserver la compatibilité	herbelin	2006-03-28
\| \| \| \| \| \| \| \|	en préparation du passage à des inductifs à polymorphisme de sorte ("sigT R" va devenir de type le type de R, càd Set) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- correction d'un bug dans coqdoc (multi_index)	notin	2006-03-28
\| \| \| \| \| \| \|	- modif. de la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8669 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug/typo dans splay_prod_assum et ajout decomp_sort	herbelin	2006-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8668 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / ↵	letouzey	2006-03-28
\| \| \| \| \| \|	OrderedType.Lt,Eq,Gt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans Coqdoc (indentation & mots clés)	notin	2006-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8666 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- correction du bug #1055	notin	2006-03-27
\| \| \| \| \| \| \| \|	- modification des propriétés sur trunk et trunk/test-suite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8665 85f007b7-540e-0410-9357-904b9bb8a0f7
*	appel Zenon sans prelude	filliatr	2006-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8664 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r8709@thot: notin \| 2006-03-25 01:48:46 +0100	notin	2006-03-25
\| \| \| \| \| \| \| \|	- Ajout de FSets dans la doc de stdlib - coqdoc copie la feuille de style dans le répertoire courant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8663 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r8708@thot: notin \| 2006-03-24 18:55:01 +0100	notin	2006-03-25
\| \| \| \| \| \| \|	Correction d'un bug sur la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8662 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r8686@thot: notin \| 2006-03-20 19:29:09 +0100	notin	2006-03-25
\| \| \| \| \| \| \|	Correction d'un bug dans Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8661 85f007b7-540e-0410-9357-904b9bb8a0f7
*	utilisation de la VM pour la normalisation finale de romega	letouzey	2006-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8660 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Patch envoy\'e par Benjamin Gregoire, permettant de corriger	letouzey	2006-03-24
\| \| \| \| \| \| \|	un probleme avec normalise_vm_in_concl git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	on ignore TAGS au niveau svn	letouzey	2006-03-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8658 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correctifs de bug pour romega:	letouzey	2006-03-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	1) dans refl_omega, on donnait a OmegaSolver un generateur de numero d'equations new_eq_id qui pouvait clasher avec les numeros d'equations initiaux créés avec new_omega_id. => on sépare en deux compteurs, un pour les equations omegas, l'autre pour les variables omegas. On en profite pour reinitialiser ces compteurs à chaque session romega, histoire que romega devienne reproductible. 2) dans omega.ml, le role de new_eq_id et new_var_id etait interverti à un endroit. ATTENTION: ceci peut changer le comportement d'omega. Surveiller le resultat du prochain bench nocturne. 3) dans ReflOmegaCore.v, on ne traitait pas le cas d'une implication dans une hypothese lors du recalcul final. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug sur 'make doc' et modification des propriétés dans doc/	notin	2006-03-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8656 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Subtac fixes, single fixpoint definitions are working again. Added a toggle ↵	msozeau	2006-03-22
\| \| \| \| \| \| \| \| \| \|	on the pretyping module to allow or disallow binding of syntaxically inexistant variables (i.e., under an if when applied to an inductive where constructors have arguments). Does not change current behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8655 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Made pretyping a functor over a coercion implementation. Pretyping.Default ↵	msozeau	2006-03-22
\| \| \| \| \| \| \| \| \| \| \|	uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction bug calcul mind_consnrealargs, introduit à la révision	herbelin	2006-03-22
\| \| \| \| \| \| \| \| \| \| \| \|	7833, et que la révision 8644 n'avait pas corrigé dans le bon sens; renommage en mind_consnrealdecls pour éviter la confusion de sens avec mind_nrealargs - Correction de la description du type one_inductive_body - Ajout test avec let-in dans params et dans type constructeur (fichier Case12.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin	2006-03-22
\| \| \| \| \| \| \| \| \| \| \|	la compilation de fichiers comme hipattern.ml (renommé en hipattern.ml4) - Extension de eqdecide.ml4 pour qu'il gère les buts sans quantificateurs, basés soient sur sumbool soit sur or, et à symétrie près de la disjunction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8652 85f007b7-540e-0410-9357-904b9bb8a0f7
*	+ destruct now works as induction on multiple arguments :	jforest	2006-03-21
\| \| \| \| \| \| \| \| \| \| \|	destruct x y z using scheme + replace c1 with c2 <in hyp> has now a new optional argument <as tac> replace c1 with c2 by tac tries to prove c2 = c1 with tac + I've also factorize the code correspoing to replace in extractactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8651 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8650 ↵	letouzey	2006-03-21
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding "New Functional Scheme"	jforest	2006-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8649 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation	herbelin	2006-03-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8648 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ documentation en syntaxe v8	herbelin	2006-03-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8647 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug BYTEFLAGS pour compilation bin/parser	herbelin	2006-03-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8646 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation mutual_inductive_body	herbelin	2006-03-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8645 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug calcul consnrealargs + bug calcul occurrences non positives + modifs ↵	herbelin	2006-03-18
\| \| \| \| \| \|	cosmétiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8644 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ debugging (et arrêt support version française)	herbelin	2006-03-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8643 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification des propriétés (svn:executable)	notin	2006-03-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout d'un debut de proprietes pour les FSetWeak	letouzey	2006-03-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8641 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deux tags $ mal formes	letouzey	2006-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8640 85f007b7-540e-0410-9357-904b9bb8a0f7
*	propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble ↵	letouzey	2006-03-16
\| \| \| \| \| \|	des fichiers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	afin que svn ignore les liens symb coqide et coqtop	letouzey	2006-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8638 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning dead code	jforest	2006-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8637 85f007b7-540e-0410-9357-904b9bb8a0f7
*	utilisation de removeA dans FSetProperties	letouzey	2006-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8636 85f007b7-540e-0410-9357-904b9bb8a0f7
*	renommage NoRedun vers le plus joli NoDup	letouzey	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8635 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	letouzey	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	letouzey	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8633 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de fonctions sur les listes	notin	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8632 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réparation de FSet (back to 8628)	notin	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8631 85f007b7-540e-0410-9357-904b9bb8a0f7
*	encore un essai	letouzey	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8630 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation des $	letouzey	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8629 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de theories/FSets contenant la partie "light" de FSets et FMap:	letouzey	2006-03-15
\| \| \| \| \| \| \| \| \| \| \| \| \|	pas d'implementations par AVL, mais celles par lists, ainsi que les foncteurs de proprietes. Au passage, ajout de MoreList (complements de List) et SetoidList (quelques relations sur des listes considerees modulo un eq ou lt non standard. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8628 85f007b7-540e-0410-9357-904b9bb8a0f7
*	+ Debugging and cleaning functional principle generation tactic	jforest	2006-03-14
\| \| \| \| \| \| \| \| \|	+ New functional induction now calls induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8627 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r8637@thot: notin \| 2006-03-14 16:00:49 +0100	notin	2006-03-14
\| \| \| \| \| \| \| \| \|	- intégration de doc dans le Makefile principal - correction d'une incompatibilité avec Tetex 3.0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8626 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r8636@thot: notin \| 2006-03-14 15:57:11 +0100	notin	2006-03-14
\| \| \| \| \| \| \|	Correction de bugs de Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8625 85f007b7-540e-0410-9357-904b9bb8a0f7