coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	backtrack unification types et deplacement make_clenv_binding	filliatr	2001-03-01
*	application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés	filliatr	2001-02-01
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin	2001-01-24
*	Renommages autour de NewInduction	herbelin	2000-12-18
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...	herbelin	2000-11-26
*	Nouveau choix pour l'intros initial	delahaye	2000-11-24
*	Renommage canonique :	herbelin	2000-10-18
*	Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...	herbelin	2000-10-13
*	nettoyage	herbelin	2000-09-10
*	Suppression de Abst	herbelin	2000-09-10
*	Retrait du i pour tclTHEN_i et correction bugs Decompose	herbelin	2000-05-16
*	Achèvement nettoyage Pfedit; ajout intros_replacing	herbelin	2000-05-05
*	Nettoyage de l'interface de Pfedit	herbelin	2000-05-04
*	Ajout du langage de tactiques	delahaye	2000-05-03
*	modules profile, Coqinit et Coqtop (=main)	filliatr	1999-12-03
*	modifs pour premiere edition de liens	filliatr	1999-12-02
*	module Tactics (debut)	filliatr	1999-11-22