coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les	herbelin	2007-09-04
\| \| \| \| \| \| \| \| \| \| \|	alias de variables dans la fonction d'inversion des instance (real_clean): - détection des cas d'inversions distinctes incompatibles - nouvelle heuristique lorsque plusieurs inversions distinctes mais compatibles existent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10111 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A word on the measure and wf modifiers	msozeau	2007-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10110 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite commit 10103 (expansion des défs locales triviales dans l'étape	herbelin	2007-09-01
\| \| \| \| \| \| \| \|	de "projection" lors de l'instanciation d'une evar -- fonction "real_clean") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fin de la correction de Function	jforest	2007-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10108 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction bug d'efficacite dans Function	jforest	2007-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10107 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server	herbelin	2007-08-30
\| \| \| \| \| \| \| \| \|	et Set Whelp Getter pour changer le nom des serveurs (report 10105 de la 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oubli dans commit 10102...	herbelin	2007-08-30
\| \| \| \| \| \| \|	+ Formattage affichage arguments evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10104 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des redéfinitions de variables (définitions locales	herbelin	2007-08-29
\| \| \| \| \| \| \| \| \|	triviales en provenance de l'algo de compilation du filtrage) lors du calcul de la projection des variables dans real_clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10103 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin	2007-08-29
\| \| \| \| \| \| \| \| \|	échouer sur les Rel liées a des Anonymous et export de l'instance des evars vers le printeur du débogueur. - Suppression d'un reste de code mort lié à la V7 dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding a few lemmas for reasoning about inequalities over the	roconnor	2007-08-28
\| \| \| \| \| \| \|	rationals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10101 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans check_and_warn	notin	2007-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10100 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oubli dans la révision 10098 (nettoyage body_of_type)	herbelin	2007-08-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug on wellfounded defs with constant parameters and dependencies on the ↵	msozeau	2007-08-26
\| \| \| \| \| \|	rec argument, example given by Brian Aydemir. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10097 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix de Bruijn bug in wf definitions.	msozeau	2007-08-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10096 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add info on measure based defs.	msozeau	2007-08-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10095 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix evars bug in mutual fixpoints with implicit types and bug in ↵	msozeau	2007-08-26
\| \| \| \| \| \|	inequalities generation for multiple patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10094 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add more equality tactics. Upgrade program_simpl for discrimination of ↵	msozeau	2007-08-26
\| \| \| \| \| \|	conjuncts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10093 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension et documentation de real_clean/evar_define dans evarutil.ml:	herbelin	2007-08-25
\| \| \| \| \| \| \| \| \| \| \| \| \|	l'unification sait maintenant résoudre des équations du genre "?n[...;x:=?m[...;y:=t;...]] = t" lorsque x et y sont uniques vérifiant cette propriété (la solution est alors de poser ?m:=y et ?n:=x); le type de t est aussi pris en compte dans cette situation (ce genre de problème permet de résoudre des cas simples d'unification avec dépendance: cf l'exemple de foldrn dans test-suite/success/Fixpoint.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10092 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et ↵	herbelin	2007-08-24
\| \| \| \| \| \|	-rectypes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation plus précise de la contrainte de type pour interpréter les	herbelin	2007-08-24
\| \| \| \| \| \| \| \| \| \| \|	points-fixes: on applique maintenant cette contrainte avant de généraliser corps et types vis à vis du context (utile notamment en présence de let-in dont on ne sait pas sinon s'ils font partie de la contrainte de type ou du contexte de typage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10088 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1634 + ajout de bugs dans la test-suite	notin	2007-08-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Save IS NOT the same Defined ....	msozeau	2007-08-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10084 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)	herbelin	2007-08-22
\| \| \| \| \| \| \|	- Des open en plus dans le débogueur-traceur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10083 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un warning losrqu'un nom de bibliothèque est ambigü	notin	2007-08-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10082 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de l'initialisation des chemins de la librairie standard	notin	2007-08-20
\| \| \| \| \| \| \| \| \|	pour imposer un ordre précis des répertoires (résout en partie le problème entre Init.Wf et Program.Wf.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10081 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo in INSTALL instructions	lmamane	2007-08-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10080 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Erreur de copier/coller dans la section Guarded	notin	2007-08-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10079 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1322	notin	2007-08-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10077 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin	2007-08-16
\| \| \| \| \| \| \| \| \|	modification de interp_ltac_reference pour passer les ids utilisées dans le contexte d'appel d'une tactique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
*	An update on axiomatic number classes.	emakarov	2007-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10075 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction (partielle) bug #1052 (coqdoc supprime les fins de ligne après ↵	notin	2007-08-13
\| \| \| \| \| \|	un commentaire) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10074 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1635	notin	2007-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10073 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un exemple d'inversion des dépendances dans le prédicat comme	herbelin	2007-08-10
\| \| \| \| \| \| \|	implicitement suggéré par le rapport de bug #1671 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10072 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction d'un bug de de Bruijn dans abstract_predicate (lié au	herbelin	2007-08-10
\| \| \| \| \| \| \| \| \| \| \| \|	rapport de bug #1671 - mais ne résoud pas le #1671 dans le propos peut être vu comme le souhait de voir traité le cas simple du problème généralement indécidable d'inversion des contraintes des types inductifs) - Petite amélioration dans le nommage des variables dans expand_arg git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10070 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	notin	2007-08-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10069 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de la test suite pour intégrer des tests spécifiques aux	notin	2007-08-10
\| \| \| \| \| \| \| \|	bugs soumis sur Coq-bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10068 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de control_only_guard, qui utilise maintenant	notin	2007-08-09
\| \| \| \| \| \| \| \| \| \| \| \|	iter_constr_with_full_binders + documentation de Guarded. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/doc/refman/RefMan-pro.tex M trunk/pretyping/inductiveops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10065 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix dependency bugs due to Program modules renamings.	msozeau	2007-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10064 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.v	emakarov	2007-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10063 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add a test case for the new "dependent" induction tactics.	msozeau	2007-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10062 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A better Program documentation. Include it in the generated stdlib doc.	msozeau	2007-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Move Program tactics into a proper theories/ directory as they are general ↵	msozeau	2007-08-07
\| \| \| \| \| \|	purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add a new tactic to generalize an instantiated inductive predicate adding ↵	msozeau	2007-08-07
\| \| \| \| \| \|	equalities. Useful to do so-called "ford" induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10059 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Build system: _really_ don't recurse into VCS metadata for file lists	lmamane	2007-08-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10058 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Build system:	lmamane	2007-08-07
\| \| \| \| \| \| \| \|	- BSD compatibility: do not use -printf action of find (2nd round) - don't recurse into VCS metadata for file lists git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10057 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Build system: BSD compatibility: do not use -printf action of find	lmamane	2007-08-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10056 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mul and sqrt	thery	2007-07-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10055 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrected the reference to glob.dump, which is used to create ↵	emakarov	2007-07-26
\| \| \| \| \| \|	stdlib/index-body.html. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10051 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add glob.dump to Makefile the recommended way and document the	lmamane	2007-07-25
\| \| \| \| \| \| \|	recommended way more explicitly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10050 85f007b7-540e-0410-9357-904b9bb8a0f7