coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	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
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
\| \| \| \| \| \| \| \|	May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
*	-Debugging multiple induction, a bug appeared when having function	courtieu	2006-03-12
\| \| \| \| \| \| \| \| \| \|	arguments to a principle (like in map_ind). -Added nbranches and npredicates to elim_scheme, and made the elimc field optional. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8622 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-03-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cleaning	jforest	2006-03-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Tutorial on recursive types	herbelin	2006-03-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8619 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r8623@thot: notin \| 2006-03-08 12:40:57 +0100	notin	2006-03-08
\| \| \| \| \| \| \|	Passage à la version LGPL de Configwin dans le trunk git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r8620@thot: notin \| 2006-03-08 11:44:16 +0100	notin	2006-03-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Modifications diverses de Coqdoc: - modification du comportement par dÃ©faut de l'option --latex - ajout d'une option --stdout - réaménagement dans les sources (création de global.ml) - modification du parser de coqdoc pour regler les problèmes liés à la syntaxe V8. - Correction du bug #1052 sur les commentaires en fin de ligne git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8617 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain ↵	jforest	2006-03-07
\| \| \| \| \| \|	is_empty in those versions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8616 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification des propriétés 'svn:ignore' pour correspondre aux .cvsignore	notin	2006-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8615 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Liste des fichiers à ignorer lors du 'svn status'	herbelin	2006-03-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8614 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de la coupure entre base et addendum (quitte à le remettre si ↵	herbelin	2006-03-03
\| \| \| \| \| \|	demandes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8613 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Inutile en svn	herbelin	2006-03-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8612 85f007b7-540e-0410-9357-904b9bb8a0f7