coq - The formal proof system

Age	Commit message (Expand)	Author
2006-02-20	Forgot another file...	coq
2006-02-20	Forgot one file	coq
2006-02-20	Change in subtac modules	coq
2006-02-20	Rewrite of the subtac tactic, needs some work on implicit arguments.	coq
2006-02-19	maj	coq
2006-02-18	maj	coq
2006-02-17	maj	coq
2006-02-17	bug correction	bertot
2006-02-17	Julien:	bertot
2006-02-17	cleaning	coq
2006-02-17	bug correction in the decomposition of an induction scheme.	coq
2006-02-17	changed the decomposition of an induction scheme	coq
2006-02-16	maj	coq
2006-02-16	added isProd to term.mli.	coq
2006-02-15	maj	coq
2006-02-15	continuing the generalization of "induction". Now induction schemes	coq
2006-02-14	maj	coq
2006-02-13	maj	coq
2006-02-13	Bug correction in saving proofs: If a hook opens a proof but does not close i...	bertot
2006-02-13	firstorder fails gracefullly when encountering untypable higher-order terms	corbinea
2006-02-12	maj	coq
2006-02-12	Bug Scope	herbelin
2006-02-12	Zmax et Zminmax	herbelin
2006-02-12	Nettoyage Zmin.v, création Zmax.v et Zminmax.v	herbelin
2006-02-12	Nettoyage Bool:	herbelin
2006-02-12	Unification max_case et max_case2	herbelin
2006-02-12	Unification min_case et min_case2	herbelin
2006-02-11	maj	coq
2006-02-11	Commentaires et compatibilité coqdoc	herbelin
2006-02-10	maj	coq
2006-02-10	induction now admits multiple induction arguments. The principle must	coq
2006-02-10	code mort	herbelin
2006-02-09	maj	coq
2006-02-09	very minor bug correction and cleanning	bertot
2006-02-09	securing intros (we now use h_intro)	bertot
2006-02-09	Minor bugs fixes	bertot
2006-02-08	maj	coq
2006-02-08	Changing Set to Type for iter.	bertot
2006-02-08	One can use a measure {mes f x} instead of a well-founded relation in GenFixp...	bertot
2006-02-08	Julien:	bertot
2006-02-08	Localisation des erreurs de sorte du prétypage	herbelin
2006-02-08	Ajout bibliothèque String de Laurent Théry	herbelin
2006-02-08	Ajout bibliothèque String de Laurent Théry	herbelin
2006-02-07	maj	coq
2006-02-07	oubli de code de debugging	herbelin
2006-02-07	Messages nth branche	herbelin
2006-02-07	Idem numbering of 'Unfold', 'simpl', ...	herbelin
2006-02-07	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin
2006-02-07	Ajout plural	herbelin
2006-02-07	Mise en conformité de l'ordre des occurrences de pattern avec l'affichage	herbelin