coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Remove bugguy notations	msozeau	2007-03-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9695 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug#1434 importing fonctor arguments, now it works.	soubiran	2007-03-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Create a program_scope in subtac Utils	msozeau	2007-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9692 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add Program keywords to coqwc	msozeau	2007-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9691 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Transparence de eq_dec et lt_dec daans OrderedTypeFacts	notin	2007-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9690 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Application suggestion #1430 de Yevgeniy pour TEXINPUTS	herbelin	2007-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9687 85f007b7-540e-0410-9357-904b9bb8a0f7
*	màj dépendances .v: SubtacTactics.vo	lmamane	2007-03-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9686 85f007b7-540e-0410-9357-904b9bb8a0f7
*	FSetInterface: new item choose_equal in the spec S (request of P. Casteran)	letouzey	2007-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9684 85f007b7-540e-0410-9357-904b9bb8a0f7
*	The right tactics for definitions using measures.	msozeau	2007-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9683 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix wf bug from F. Besson and work on ineqs generation.	msozeau	2007-02-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9682 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revision of the coqide configuration:	letouzey	2007-02-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* if -byte-only is used, then -coqide byte is implied except when the user explicitely said otherwise * If the user asks -coqide opt or byte, then LablGtk2 checks are not bypassed anymore. In particular, the check whether ide/undo.mli should be compatible with LablGtk2 < 2.6.0 or >= 2.6.0 is done. * The tests are organized in a linear sequence of "if elif elif else" that the next reader of this code may have a chance to understand git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9681 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug de l'install (win)	notin	2007-02-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9680 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Une passe sur les warnings (ajout Options.warn déclenchée par ↵	herbelin	2007-02-24
\| \| \| \| \| \| \| \| \|	compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles + messages divers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)	herbelin	2007-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9678 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin	2007-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Améliorations utiles pour les Makefile répartis sur plusieurs répertoires	herbelin	2007-02-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coqdep : - fonction de "canonisation" du nom des cibles plus performante (elle traverse notamment les "..") coq_makefile : - ajout automatique de "-I ." dans COQLIBS seulement si pas déjà déclaré (utile pour éviter les cibles en double dans coqdep en présence de -R) - explicitation de "-byte" dans la cible "byte:" (son absence semble remonter à l'époque où l'exécution en byte était le défaut) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9676 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Opacity parameterization for obligations working.	msozeau	2007-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9675 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Debug wellfounded defs, work on cleaning obls envs	msozeau	2007-02-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9674 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin	2007-02-22
\| \| \| \| \| \| \| \|	"R ?1 ... ?n <= T". Utilisation de cette fonction dans Setoid_replace au au lieu de w_unify (suggestion de GG). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9673 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish ↵	notin	2007-02-22
\| \| \| \| \| \|	#1375) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9672 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc: typo/english: "is left associating" -> "is left-associative".	lmamane	2007-02-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9671 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of tactical "t1 \|\| t2": t2 is executed if t1 fails to	lmamane	2007-02-22
\| \| \| \| \| \| \|	progress, not only if it fails (i.e. gives an error). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9670 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin	2007-02-21
\| \| \| \| \| \| \|	+ petit nettoyage himsg.ml + petite uniformisation erreurs CannotUnify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9668 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction typo liée au commit 8779 (levait une anomalie)	herbelin	2007-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9666 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin	2007-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9664 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed some useless code in mod_typing that was redundant with safe_typing.	soubiran	2007-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9663 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran	2007-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9662 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correct coq depend, add eq_rect elimination tactic to SubtacTactics	msozeau	2007-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9661 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajouts de lemmes dans Min et Max	notin	2007-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9660 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Various little subtac fixes, add some useful tactics.	msozeau	2007-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compilation de la FAQ	notin	2007-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.	msozeau	2007-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9656 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.	msozeau	2007-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9655 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Missing keyword	msozeau	2007-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9654 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lift params appropriately, do not need to coerce to tycon	msozeau	2007-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9653 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add functionality to permit printing terms with references to anonymous ↵	msozeau	2007-02-16
\| \| \| \| \| \|	variables, useful for debugging git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9652 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update implementation for dependent types. Works just as well as before for ↵	msozeau	2007-02-16
\| \| \| \| \| \|	simple cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9651 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors	herbelin	2007-02-15
\| \| \| \| \| \| \|	du passage de l'ancienne à la nouvelle syntaxe) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réparation absence d'interprétation des liaisons vers listes	herbelin	2007-02-15
\| \| \| \| \| \| \|	d'occurrences (clause "at") dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9648 85f007b7-540e-0410-9357-904b9bb8a0f7
*	encodage des types	filliatr	2007-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9646 85f007b7-540e-0410-9357-904b9bb8a0f7
*	tactique yices	filliatr	2007-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9645 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
\| \| \| \| \| \| \| \|	fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug mineur dans la generation des principes d'induction pour Function	jforest	2007-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9643 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Autres passages de Set Ã Type dans Relations et Wellfounded	herbelin	2007-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix matching on dependent types, taking a safe stand.	msozeau	2007-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9641 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans la génération des principes d'induction	jforest	2007-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add keywords that were missing, notably for terms.	msozeau	2007-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9638 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppresion de la catégorie des inductifs singletons larges dont	herbelin	2007-02-09
\| \| \| \| \| \| \| \|	l'élimination vers Set était autorisée: comme souligné par Benjamin, c'est incompatible avec EM + AC (report rev 9633 8.1) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugfix suffices	corbinea	2007-02-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9632 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retour r9310 en attendant mieux	herbelin	2007-02-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9629 85f007b7-540e-0410-9357-904b9bb8a0f7