coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	preparation pour release (suite)	barras	2004-03-15
*	To make that the translation process does not fail on data produced by	bertot	2004-03-15
*	oops	corbinea	2004-03-15
*	minor changes	corbinea	2004-03-14
*	congruence now handles disequalities	corbinea	2004-03-14
*	Mise en place temporaire d'un afficheur de 'language' pour le traducteur	herbelin	2004-03-13
*	Ooops ! bug in firstorder fixed (let's hope no one noticed)	corbinea	2004-03-11
*	reals: renamed type option into field_rel_option	marche	2004-03-11
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Reparation ROmega V8/Omega ZERO/POS/NEG	mohring	2004-03-04
*	adaptation V8 version Pierre Cregut	mohring	2004-03-03
*	takes better account of the new possibility to pass a parametric count argument	bertot	2004-03-03
*	removes capital letters in two tactic names.	bertot	2004-03-03
*	make sure the implicit argument indications are in the right order	bertot	2004-03-03
*	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin	2004-03-02
*	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin	2004-03-02
*	code mort	herbelin	2004-03-01
*	Ajout IntroPattern comme type d'argument générique	herbelin	2004-03-01
*	Protection d'un 'clear' qui peut etre dependant	herbelin	2004-03-01
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
*	Not all cases for coercions and locality were handled	bertot	2004-02-26
*	corrects the treatement of SubClass declarations	bertot	2004-02-23
*	makes sure the following examples are well-treated:	bertot	2004-02-19
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	accomodate the .. extension	bertot	2004-02-16
*	adds a new command for searching a pattern inside the premises of theorems	bertot	2004-02-16
*	corrects a bug in name reservation, simplifies or_intro, removes dead code	bertot	2004-02-16
*	petit bug avec Extraction Optimize	letouzey	2004-02-13
*	adds a new command add_rec_path for the parser program and changes add_path	bertot	2004-02-13
*	adds the possibility to have terms (and not just identifiers) as hints	bertot	2004-02-13
*	adds the possibility to have terms (and not just identifiers) as hints	bertot	2004-02-13
*	lazy was translated to cbv, obviously wrong	bertot	2004-02-12
*	Implicits can have an optional list of argument, which is different	bertot	2004-02-12
*	a new version that uses intro patterns, but the code still needs some cleaning	bertot	2004-02-11
*	removes a lot comments that may be useful for later code maintenance, but	bertot	2004-02-11
*	Correction of a bug in Functional Scheme discovered when porting the	coq	2004-02-10
*	New version of Functional Scheme and functional induction. Deals with	coq	2004-02-09
*	correction de bugs de congruence et firstorder (inductifs)	corbinea	2004-02-06
*	adds the possibility to mark function arguments as formulas in Ltac	bertot	2004-02-02
*	adds the possibility to mark function arguments as formulas in Ltac	bertot	2004-02-02
*	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
*	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
*	make sure that 'in' clauses for reduction tactics are translated	bertot	2004-01-28
*	a try to make intro patterns better	bertot	2004-01-26
*	streamlines the keywords for definitions, require commandsbinders, notation	bertot	2004-01-24
*	change add path commands to get the extra argument and the Hint commands	bertot	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