coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	License de contrib/interface	herbelin	2004-06-29
*	contrib/interface $$@!	corbinea	2004-06-28
*	Modules et Records: gros changements pour prendre en compte le nouveau mind_r...	letouzey	2004-06-28
*	Licence changed from GPL to Lesser GPL.	sacerdot	2004-06-26
*	eq and eqT are the same	barras	2004-06-25
*	correspondance des records et noms de champs de records entre un module et sa...	letouzey	2004-06-25
*	Retour sur amendement de l'interprétation mult sur nat (bug 743) car incompa...	herbelin	2004-05-28
*	"comments only" commit.	coq	2004-05-13
*	Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est de...	herbelin	2004-05-07
*	pb install de pcoq	barras	2004-04-21
*	Copyright notice of files in contrib/xml made uniform.	sacerdot	2004-04-07
*	Old file. The new version of this script is no longer distributed with	sacerdot	2004-04-07
*	- theoryobject.dtd is the DTD for .theory files	sacerdot	2004-04-07
*	Loic code to pretty-print the generated proof-tree debranched (since it	sacerdot	2004-04-07
*	CoRN CProp detection improved: products of "sort" CProp are now recognized	sacerdot	2004-04-07
*	Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;	sacerdot	2004-04-07
*	Fake dependent products in inductive definition types are no longer replaced	sacerdot	2004-04-06
*	Important bug fix: since coqdoc is now quoting XML reserved characters in	sacerdot	2004-04-06
*	Since coqdoc produces (X)HTML, HTML character entities can be used	sacerdot	2004-04-05
*	correction rapide du bug PR\#592	letouzey	2004-04-05
*	WARNING	sacerdot	2004-04-04
*	LocalFact added as a choice for the "as" attribute of ht:VARIABLE in the	sacerdot	2004-04-01
*	Big bug fixed: interactive local definitions where handled as constants	sacerdot	2004-04-01
*	Output of theory files reimplemented using Buffer.	sacerdot	2004-04-01
*	~keep_sections was now redundant. Got rid of.	sacerdot	2004-04-01
*	En mode batch, recuperation via Declare de l'information si un inductive est ...	herbelin	2004-03-31
*	Fake dependent types in constructors of inductive types are now preserved.	sacerdot	2004-03-31
*	* WARNING: DTD Change *	sacerdot	2004-03-30
*	declare_internal_constant behaved as declare_constant for proofs (e.g.	sacerdot	2004-03-30