coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot	2005-05-20
*	added VernacBacktrack (new backtracking command dedicated to	coq	2005-05-19
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Allow auto to have a parametric argument (wish #967)	herbelin	2005-05-15
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin	2005-03-07
*	Renaming Print Canonical Structure into Print Canonical Projections	herbelin	2005-02-18
*	Standardisation of function names about global references (especially, renami...	herbelin	2005-02-18
*	Ajout Print Canonical Structures	herbelin	2005-02-12
*	Nettoyage et documentation de Library	herbelin	2005-02-06
*	Ajout cas VernacBackTo	herbelin	2005-01-26
*	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot	2005-01-13
*	- Module/Declare Module syntax made more uniform:	sacerdot	2005-01-06
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-24
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin	2004-12-06
*	Correction 1.138 appliquée à tort à la branche principale au lieu de V8-0b...	herbelin	2004-11-29
*	Commit précédent erroné; retour version précédente	herbelin	2004-11-29
*	MAJ vis à vis de extratactics	herbelin	2004-11-28
*	Locate Module	herbelin	2004-11-17
*	New command "Print Rewrite HindDb dbname".	sacerdot	2004-11-17
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin	2004-10-11
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	Ajout de or-pattern pour le match-with v8	herbelin	2004-09-09
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	"Show Setoids" command added.	sacerdot	2004-07-23
*	Abstraction vis a vis du type loc pour ocaml 3.08	herbelin	2004-07-18
*	Nouvelle en-tête	herbelin	2004-07-16
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	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