coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Finalement, scopes utiles pour option 'where' (cf bug #1132)	herbelin	2006-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8689 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Documentation of the Program tactics.	msozeau	2006-04-07
\| \| \| \| \| \| \| \| \| \|	- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
*	versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes	letouzey	2006-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8687 85f007b7-540e-0410-9357-904b9bb8a0f7
*	versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes	letouzey	2006-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8686 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ouverture du bon scope (positive_scope) derriere le constructeur Npos de N	letouzey	2006-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8685 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Enlevement de message d'erreur garbage.	courtieu	2006-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8684 85f007b7-540e-0410-9357-904b9bb8a0f7
*	resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses	letouzey	2006-04-05
\| \| \| \| \| \| \| \|	avec des equivalences parametrees (genre forall n, P n <-> Q n) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8683 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ Licence FAQ	herbelin	2006-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8682 85f007b7-540e-0410-9357-904b9bb8a0f7
*	on utilise explicitement Prop/iff pour certains morphismes pour eviter des ↵	letouzey	2006-04-05
\| \| \| \| \| \|	warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8681 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression du test Proof with <tac>	notin	2006-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8680 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout d'un rattrapage d'erreur pour "induction using".	courtieu	2006-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8679 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug index addendum à cause mauvaise utilisation asection dans Helm.tex	herbelin	2006-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8678 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug 1119 (inversion marche a moitie dans Type)	herbelin	2006-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petite actualisation FAQ	herbelin	2006-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8676 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amendement impression evar pour affichage des Meta par 'info'	herbelin	2006-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8675 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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