coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	updates the definition of tactics using Ltac and adds the subst tactic	bertot	2004-01-30
*	adds module commands and update the extration command	bertot	2004-01-30
*	maj	filliatr	2004-01-30
*	maj	filliatr	2004-01-30
*	pour win32	coq	2004-01-29
*	Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...	herbelin	2004-01-29
*	Reparation d'une rupture (en presence de types implicites) de l'invariant que...	herbelin	2004-01-29
*	pour ide sous windows	coq	2004-01-29
*	MAJ	herbelin	2004-01-29
*	Suppression de 'Print.' en v8	herbelin	2004-01-29
*	RÃ©utilisation de VernacSyntacticDefinition pour diffÃ©rencier "Notation id :...	herbelin	2004-01-29
*	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