coq - The formal proof system

Age	Commit message (Expand)	Author
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
2007-02-07	Suppression RefMan-cas.tex inutilisé	herbelin
2007-02-07	Backtrack sur le passage de Set à Type pour l'ordre lexicographique	herbelin
2007-02-07	Various subtac fixes. Add inequalities in pattern matching branches when need...	msozeau
2007-02-07	Field rewrites only with polynomial	thery
2007-02-07	doc de ring/field + option infinite -> completeness	barras
2007-02-06	Report de la révision 9599 de la v8.1 dans le trunk	notin
2007-02-06	Passage de Set à Type dans Relations et Wellfounded	herbelin
2007-02-06	doc for field	thery
2007-02-05	complement du commit 9591	bgregoir
2007-02-05	changement dans ring specification du sign, division	bgregoir
2007-02-03	Work on ineqs generation.	msozeau
2007-02-02	Factorisation de la règle Constr.binder dans g_subtac.ml pour éviter	herbelin
2007-02-02	field: introduction de Get_goal	bgregoir
2007-02-02	ring: introduction de Get_goal	bgregoir
2007-02-02	Now 1/x * x simplifies to 1	thery