coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise p...	herbelin	2004-12-27
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-24
*	Hugo fixed a bug of refine, and it revealed a bug of functional	coq	2004-12-10
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	travail sur les types extraits	letouzey	2004-12-09
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	Code mort	herbelin	2004-12-06
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin	2004-12-06
*	Orthographe!	herbelin	2004-12-03
*	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
*	When a reference to a constructor is met its inductive type must be closed.	sacerdot	2004-11-18
*	Locate Module	herbelin	2004-11-17
*	New command "Print Rewrite HindDb dbname".	sacerdot	2004-11-17
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin	2004-10-11
*	Suppression IsConjecture redondant avec Conjectural	herbelin	2004-10-11
*	un paquet de corrections de bugs	letouzey	2004-10-04
*	The "Add Setoid" command now has a new argument "as name" that is used	sacerdot	2004-10-01
*	cutrewrite does not work with relations that are not Coq-like equalities.	sacerdot	2004-09-30
*	New syntax	sacerdot	2004-09-29
*	firstorder bugfix to cope with elim of sigma types with goal is of the wrong ...	corbinea	2004-09-27
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	Ajout de or-pattern pour le match-with v8	herbelin	2004-09-09
*	The innersort is now computed as the more precise sort between the	sacerdot	2004-09-08
*	The code used to compare the synthesized and the expected type (if available)	sacerdot	2004-09-08
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	reparation des Extract Constant avec Haskell	letouzey	2004-09-06
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Ported to the new implementation of setoid_*.	sacerdot	2004-09-03
*	The old implementation of (setoid_replace c1 with c2) used to replace	sacerdot	2004-09-03
*	Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1	herbelin	2004-08-24
*	Setoid_replace.setoid_replace: last argument (that was supposed to be	sacerdot	2004-07-23
*	"Show Setoids" command added.	sacerdot	2004-07-23
*	correction d'un bug de la tactique pour les semi setoid rings.	clrenard	2004-07-22
*	Protection des accès tableau car, sur Sparc-linux, cela engendre une erreur ...	herbelin	2004-07-19
*	Abstraction vis a vis du type loc pour ocaml 3.08	herbelin	2004-07-18
*	Nouvelle en-tête	herbelin	2004-07-16
*	ajout des unsafeCoerce + 2 bugs haskell	letouzey	2004-07-14
*	* <style>...</style> tag no longer generated for theory files	sacerdot	2004-07-08
*	- recent changes to doubleTypeInference.ml (that introduced double	sacerdot	2004-07-08
*	Commit to perform double type inference also on inner types.	sacerdot	2004-07-08
*	Constants just after a "Let id : t. ... Qed" local variable declaration were	sacerdot	2004-07-05
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30