coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran	2007-02-21
*	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-19
*	Compilation de la FAQ	notin	2007-02-18
*	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-16
*	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-15
*	encodage des types	filliatr	2007-02-14
*	tactique yices	filliatr	2007-02-14
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	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-12
*	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-11
*	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-09
*	Add lif then else for if in bool.	msozeau	2007-02-08
*	Fix myinjection tactic, generalize coercion for applications	msozeau	2007-02-08
*	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-07
*	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-06
*	complement du commit 9591	bgregoir	2007-02-05
*	changement dans ring specification du sign, division	bgregoir	2007-02-05
*	Work on ineqs generation.	msozeau	2007-02-03
*	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	2007-02-02
*	Report de révision 9583 de la v8.1 dans le trunk	notin	2007-02-01