coq - The formal proof system

Age	Commit message (Expand)	Author
2016-09-16	Addressing OCaml compilation warnings.	Hugo Herbelin
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-07-01	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès
2016-06-24	Optimize the subst tactic.	Pierre-Marie Pédrot
2016-06-05	Removing the Q_constr file.	Pierre-Marie Pédrot
2016-06-05	Moving Hipattern to a regular ML file.	Pierre-Marie Pédrot
2006-03-22	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-11-02	Types inductifs parametriques	mohring
2004-07-16	Nouvelle en-tête	herbelin
2004-03-11	code obsolete	herbelin
2003-06-20	Ground Update.	corbinea
2003-05-25	Ground and CCsolve updates	corbinea
2003-05-19	Restructuration des procédures de filtrage	herbelin
2003-05-07	Enhancement of the Ground tactic, addition of GTauto and GIntuition.	corbinea
2003-04-25	Added the Ground tactic.	corbinea
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2002-11-14	JMeq now treated as an equality by tactics.	courant
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-05-22	Correction of a bug in Intuition (no more decomposition of dependent pairs).	corbinea
2002-02-14	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras
2001-11-05	GROS COMMIT:	barras
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-09-13	eclaircissement du code	courant
2001-03-15	entetes	filliatr
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-06	Correction incompatibilites dans la fn des types des inductifs	herbelin
2000-10-01	Renommage AppL en App	herbelin
2000-09-14	Abstraction de constr	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-06-15	Code mort	herbelin
2000-05-31	Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs	herbelin
2000-05-18	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin
2000-05-03	Ajout get_reference	herbelin
2000-05-02	Divers	herbelin
2000-04-30	Suite intégration de constr_pattern	herbelin
2000-04-28	Decoupage de tactics/pattern en proofs/pattern et tactics/hipattern	herbelin