coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	updates the tactics contradiction and autorewrite, the commands	bertot	2004-01-29
*	maj	filliatr	2004-01-29
*	Bug de Require multiple	herbelin	2004-01-28
*	make sure that 'in' clauses for reduction tactics are translated	bertot	2004-01-28
*	maj	filliatr	2004-01-28
*	maj	filliatr	2004-01-28
*	Bug activation erronÃ©e du traducteur en v8	herbelin	2004-01-27
*	meilleure separation de compil et install de coq, coqide et coq-interface	barras	2004-01-27
*	Correction des cibles des theories indviduelles	herbelin	2004-01-27
*	MAJ simplification	herbelin	2004-01-27
*	Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...	herbelin	2004-01-27
*	Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...	herbelin	2004-01-27
*	maj	filliatr	2004-01-27
*	maj	filliatr	2004-01-27
*	deplacement des cma et cmxa dans les sous-repertoires	barras	2004-01-26
*	reparation de qqs bugs du traducteur	barras	2004-01-26
*	a try to make intro patterns better	bertot	2004-01-26
*	maj	filliatr	2004-01-26
*	maj	filliatr	2004-01-26
*	streamlines the keywords for definitions, require commandsbinders, notation	bertot	2004-01-24
*	maj	filliatr	2004-01-24
*	MAJ	herbelin	2004-01-23
*	Bug induction lors de types inductives avec parametres	herbelin	2004-01-23
*	maj	filliatr	2004-01-23
*	change add path commands to get the extra argument and the Hint commands	bertot	2004-01-22
*	Correction lecture des locations si pas demandees dans l'ordre	herbelin	2004-01-22
*	Protection table des locations lors de Load (pour coqdoc)	herbelin	2004-01-22
*	fixes argument lists for tactic definitions, updates inversion tactics	bertot	2004-01-22
*	adds a clause argument to symmetry	bertot	2004-01-22
*	corrects the way the structural argument declaration is handled in	bertot	2004-01-22
*	adds the notations in inductive definitions, improves the consistency between	bertot	2004-01-22
*	handles explicit function calls, names meta variables in patterns	bertot	2004-01-22
*	maj	filliatr	2004-01-22
*	maj	filliatr	2004-01-22
*	MAJ	herbelin	2004-01-21
*	Export information des references et location de notations pour coqdoc	herbelin	2004-01-21
*	Export information des references de notations pour coqdoc	herbelin	2004-01-21
*	Deplacement lexer pour dependance dans constrintern	herbelin	2004-01-21
*	updates the structure of fix (struct argument added) and if	bertot	2004-01-21
*	MAJ	herbelin	2004-01-21
*	maj	filliatr	2004-01-21
*	coqide utf8	marche	2004-01-20
*	Le traducteur utilisait un afficheur des reels obsolete et bugge	herbelin	2004-01-20
*	Suppression 'Implicit Arguments On/Off' qui n'a plus lieu d'etre en v8	herbelin	2004-01-20
*	maj	filliatr	2004-01-20
*	handles projector notations, cases with return types,	bertot	2004-01-19
*	1.20	bertot	2004-01-19
*	1.19	bertot	2004-01-19
*	adds constructs to handle notations in patterns	bertot	2004-01-19
*	maj	filliatr	2004-01-19