coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	License de contrib/interface	herbelin	2004-06-29
*	contrib/interface $$@!	corbinea	2004-06-28
*	pb install de pcoq	barras	2004-04-21
*	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
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	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
*	Ajout IntroPattern comme type d'argument générique	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
*	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
*	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
*	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
*	updates the structure of fix (struct argument added) and if	bertot	2004-01-21
*	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
*	translation to structures now okay for pattern matching constructs	bertot	2004-01-15
*	compact nested universal quantifications into a single quantification with	bertot	2004-01-14
*	make sure the parser for FORMULA does not require them to be enclosed in	bertot	2004-01-14