coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish #...	notin	2007-02-22
*	Correct coq depend, add eq_rect elimination tactic to SubtacTactics	msozeau	2007-02-19
*	Various little subtac fixes, add some useful tactics.	msozeau	2007-02-19
*	Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.	msozeau	2007-02-16
*	lift params appropriately, do not need to coerce to tycon	msozeau	2007-02-16
*	Update implementation for dependent types. Works just as well as before for s...	msozeau	2007-02-16
*	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
*	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
*	Retour r9310 en attendant mieux	herbelin	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
*	Various subtac fixes. Add inequalities in pattern matching branches when need...	msozeau	2007-02-07
*	doc de ring/field + option infinite -> completeness	barras	2007-02-07
*	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
*	Abbreviation of order notation.	msozeau	2007-02-01
*	constr_of_pat bug with nested patterns.	msozeau	2007-01-30
*	Various fixes in subtac, update some test cases.	msozeau	2007-01-29
*	Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.	msozeau	2007-01-29
*	"suffices" implemented + syntax cleanup	corbinea	2007-01-28
*	Contounement d'un probleme avec la VM dans Function	jforest	2007-01-26
*	Update some tests and fix section bug.	msozeau	2007-01-24
*	changement de la fonction norm_subst	bgregoir	2007-01-24
*	ring : Correction du bug PR#1306	bgregoir	2007-01-23
*	Correction du bug #1315:	notin	2007-01-22
*	Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouent	herbelin	2007-01-22
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
*	Various subtac fixes.	msozeau	2007-01-15
*	Suite au mail de Lionel a propos du Makefile:	letouzey	2007-01-12
*	un saut de ligne ...	letouzey	2007-01-12
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Subtac fixes, support for reasoning on wf defs.	msozeau	2007-01-08
*	suite de la reparation du bug 1239: apres les inds, les records et vars de types	letouzey	2007-01-05
*	Rework subtac pattern matching equalities generation.	msozeau	2007-01-02
*	Remplacement de la définition de Pind et Prec par une définition	herbelin	2006-12-28
*	Default tactic for solving goals.	msozeau	2006-12-22
*	typo malencontreuse	filliatr	2006-12-21