coq - The formal proof system

Age	Commit message (Expand)	Author
2007-02-27	Revision of the coqide configuration:	letouzey
2007-02-27	Correction d'un bug de l'install (win)	notin
2007-02-24	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin
2007-02-24	Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)	herbelin
2007-02-24	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin
2007-02-24	Améliorations utiles pour les Makefile répartis sur plusieurs répertoires	herbelin
2007-02-24	Opacity parameterization for obligations working.	msozeau
2007-02-23	Debug wellfounded defs, work on cleaning obls envs	msozeau
2007-02-22	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin
2007-02-22	Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish #...	notin
2007-02-22	doc: typo/english: "is left associating" -> "is left-associative".	lmamane
2007-02-22	Documentation of tactical "t1 \|\| t2": t2 is executed if t1 fails to	lmamane
2007-02-21	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin
2007-02-21	Correction typo liée au commit 8779 (levait une anomalie)	herbelin
2007-02-21	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin
2007-02-21	Removed some useless code in mod_typing that was redundant with safe_typing.	soubiran
2007-02-21	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran
2007-02-19	Correct coq depend, add eq_rect elimination tactic to SubtacTactics	msozeau
2007-02-19	Ajouts de lemmes dans Min et Max	notin
2007-02-19	Various little subtac fixes, add some useful tactics.	msozeau
2007-02-18	Compilation de la FAQ	notin
2007-02-16	Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.	msozeau
2007-02-16	Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.	msozeau
2007-02-16	Missing keyword	msozeau
2007-02-16	lift params appropriately, do not need to coerce to tycon	msozeau
2007-02-16	Add functionality to permit printing terms with references to anonymous varia...	msozeau
2007-02-16	Update implementation for dependent types. Works just as well as before for s...	msozeau
2007-02-15	Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors	herbelin
2007-02-15	Réparation absence d'interprétation des liaisons vers listes	herbelin
2007-02-14	encodage des types	filliatr
2007-02-14	tactique yices	filliatr
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-12	Bug mineur dans la generation des principes d'induction pour Function	jforest
2007-02-12	Autres passages de Set Ã Type dans Relations et Wellfounded	herbelin
2007-02-12	Fix matching on dependent types, taking a safe stand.	msozeau
2007-02-11	Correction d'un bug dans la génération des principes d'induction	jforest
2007-02-11	Add keywords that were missing, notably for terms.	msozeau
2007-02-09	Suppresion de la catégorie des inductifs singletons larges dont	herbelin
2007-02-09	bugfix suffices	corbinea
2007-02-09	Retour r9310 en attendant mieux	herbelin
2007-02-09	Report de la révision r9605 de la branche v8.1 vers le trunk (abstract récu...	notin
2007-02-09	Separate Tactics in subtac.	msozeau
2007-02-08	Add lif then else for if in bool.	msozeau
2007-02-08	Fix myinjection tactic, generalize coercion for applications	msozeau
2007-02-07	Fix mistake naming my Tactics file Tactics :)	msozeau
2007-02-07	Add tactics for induction on subterms.	msozeau
2007-02-07	Meilleur anglais (cf 9619)	herbelin
2007-02-07	Vérification que toutes les evars ont étés instanciées dans les types imp...	herbelin
2007-02-07	Correction bug #1364 (les variables de section sont repérées par	herbelin
2007-02-07	Relecture/nettoyage chapitre Gallina; déplacement section Function	herbelin