coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update for v8.1	lmamane	2007-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Move definition of VO_TOOLS_DEP before first use of it.	lmamane	2007-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9498 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reintroduce compatibility with old versions of GNU make	lmamane	2007-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1282	herbelin	2007-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9495 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1302	herbelin	2007-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction adresse CoRN dans FAQ (suite)	herbelin	2007-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9492 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction adresse CoRN dans FAQ (cf #1317)	herbelin	2007-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9491 85f007b7-540e-0410-9357-904b9bb8a0f7
*	README update:	lmamane	2007-01-17
\| \| \| \| \| \| \| \| \| \|	- GNU Make version 3.80 or later is needed. - a C compiler is needed. - not all ./configure options are listed, refer people to "./configure -help". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9487 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Various subtac fixes.	msozeau	2007-01-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9485 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite au mail de Lionel a propos du Makefile:	letouzey	2007-01-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	1) Disparition de test_extraction.v rebasculé dans test-suite/success/extraction.v Au passage, remplacement de quelques Set en Type pour ne pas avoir besoin du -impredicative-set. Et ajout de passes d'extraction en Haskell et Scheme. Simplification du Makefile en conséquence (plus de barestate) 2) Au passage, reparation (et embellissement) de extract_env. Depuis le passage de Claudio dans cette portion (il y a 2 ans ?), faire Extraction S (ou tout autre constructeur) echouait. Idem pour un nom d'inductif mutuel autre que le premier du paquet. Etonnant que personne n'ait remarqué ca plus tot... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un saut de ligne ...	letouzey	2007-01-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9483 85f007b7-540e-0410-9357-904b9bb8a0f7
*	addition du neq unicode	letouzey	2007-01-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9482 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petit oubli dans commit 9474	herbelin	2007-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9480 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une option de débogage pour expliciter l'instance des evars	herbelin	2007-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9479 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Make .vo files depend on coqdoc if COQ_XML is set (bug #848)	lmamane	2007-01-10
\| \| \| \| \| \| \| \|	- Clean up NO_RECOMPILE_LIB treatment a bit - Clean up .vo dependencies in general git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Merge with Lionel Elie Mamane's private branch:	lmamane	2007-01-10
\| \| \| \| \| \| \| \|	- Fix previous merge (semantic/type conflict in code added minutes before my commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9477 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Makefile: Option (environment variable NO_RECOMPILE_LIB) to not recompile the whole standard library just because the coq binaries got rebuilt. - Infrastructure to change the object pretty-printers at runtime. - Use that infrastructure to make coqtop-protocol with Pcoq trees and Pcoq-protocol with pretty-printed terms possible in coq-interface. - Make "Back(track)" into closed sections, modules and module types "Just Work™". - Modernise/generalise Pcoq protocol a bit, make some of its warts optional. - Implement "Show." in Pcoq mode. - Add Rpow_def.vo to REALSBASEVO so that its dependencies are computed (and used). - "make revision" now handles GNU Arch / tla in addition to svn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite commit restructuration discharge (application du type de	herbelin	2007-01-10
\| \| \| \| \| \| \|	discharge_function des implicites au cas des scopes d'arguments) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Avant : une unique méthode discharge_function qui avait accès à l'ancien environnement mais pas de possibilité de raisonner avec les objets du nouvel environnement en cours de construction. C'était problématique pour le discharge des implicites, arguments scope, etc qui étaient finalement faits en même temps que le discharge des constantes et inductifs mais avec pour effets de bord que les entrées dans la lib_stk arrivaient juste avant celles des constantes et inductifs avec des problèmes pour effacer les bonnes entrées au moment du reset - Maintenant : deux méthodes distinctes : discharge_function qui est appliquée pour collecter de l'ancien environnement ce qui est à garder dans la section et rebuild_function qui reconstruit le nouvel environnement connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant l'extensibilité que la méthode ancienne du fichier discharge.ml ne permettait pas) Au passage, ajout d'un modificateur Global aux déclarations d'implicites et d'arguments scopes pour indiquer qu'elles doivent perdurer à la sortie de la section Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps discharged reste) Au passage, nettoyage impargs.ml, suppression code mort résiduel du traducteur etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Subtac fixes, support for reasoning on wf defs.	msozeau	2007-01-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9473 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite de la reparation du bug 1239: apres les inds, les records et vars de types	letouzey	2007-01-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9471 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rework subtac pattern matching equalities generation.	msozeau	2007-01-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9470 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add f_equal case for 6 arguments.	msozeau	2007-01-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre une source possible de liaison de lambda anonyme	herbelin	2006-12-29
\| \| \| \| \| \| \|	(utilisation du nom de la contrainte de type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9468 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
\| \| \| \| \| \| \|	égalité décidable + maj dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction petits bugs du check de la test-suite	herbelin	2006-12-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9466 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de la définition de Pind et Prec par une définition	herbelin	2006-12-28
\| \| \| \| \| \| \| \| \|	suggérée par Conor McBride qui ne fait pas intervenir eq_rect et qui permet de montrer "facilement" (mais avec l'axiome K) les équations de réduction de Prec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9465 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning backtracking code, optimized "Backtrack n x y" when n is	courtieu	2006-12-28
\| \| \| \| \| \|	current state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Report correction bug #1289 dans trunk (r9435 pour branche v8.1)	herbelin	2006-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Doc for Combined Scheme.	msozeau	2006-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9462 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Addition of a "Combined Scheme" vernacular command for building the ↵	msozeau	2006-12-23
\| \| \| \| \| \| \| \| \|	conjunction of mutual inductions principles. e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9461 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Default tactic for solving goals.	msozeau	2006-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9460 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remplacement d'un test d'egalite par un test de convertibilite dans ↵	jforest	2006-12-22
\| \| \| \| \| \|	injection/discriminate/inversion pour corriger des bugs en presence de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9459 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typo malencontreuse	filliatr	2006-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adaptation à Subversion 1.4	notin	2006-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9457 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation bug 1239	letouzey	2006-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9455 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement dans ring et field, beaucoup de correction d'erreurs,	bgregoir	2006-12-15
\| \| \| \| \| \| \| \| \|	maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
*	contrib/dp: tactique ergo (voir ergo.lri.fr)	filliatr	2006-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9453 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Confusion sur le paramètre à donner à concrete_name lors du commit 9450	herbelin	2006-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9452 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reimplemented equality generation for pattern matching at typing time. First ↵	msozeau	2006-12-14
\| \| \| \| \| \|	version. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9451 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin	2006-12-13
\| \| \| \| \| \| \| \|	résoudre la clause with de apply/elim) sur la politique de renommage de concrete_name git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9450 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test condition de garde	barras	2006-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9449 85f007b7-540e-0410-9357-904b9bb8a0f7
*	svn:ignore	herbelin	2006-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9448 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin	2006-12-13
\| \| \| \| \| \| \| \|	terme arbitraire, possiblement dépendant, qui a été transformé en let-in (cf success/destruct.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9447 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1273, deuxième version (avec des shémas d'elimination ↵	notin	2006-12-12
\| \| \| \| \| \|	plus simples) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1273 (problème avec les paramètres non récursivement ↵	notin	2006-12-12
\| \| \| \| \| \|	uniformes dans le cas de types mutuellement inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9445 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Subtac: work on cases.	msozeau	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9444 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvelle indentation des scripts	barras	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9443 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cosmetique	barras	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9442 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Variable print_instances pour dÃ©boguer les instances d'evar	herbelin	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9441 85f007b7-540e-0410-9357-904b9bb8a0f7