coq - The formal proof system

Age	Commit message (Expand)	Author
2008-06-14	Correction bug 1878 (utilisation de extend_evar déplacée là où une	herbelin
2008-06-11	Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-05-28	introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...	barras
2008-05-12	Changement de stratégie vis à vis du commit 10859 sur la gestion des	herbelin
2008-05-10	- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des	herbelin
2008-04-30	Réutilisation de l'infrastructure pour le polymorphisme d'univers des	herbelin
2008-04-28	Petites corrections vis à vis des commits 10860, 10859, 10850	herbelin
2008-04-27	Correction du bug des types singletons pas sous-type de Set	herbelin
2008-03-17	* Factorizing code : context_chop was used in several files (even as chop_con...	vsiles
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-08-27	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin
2007-06-30	- Ajout de la possibilité d'utiliser la notation Record pour les	herbelin
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2006-12-14	Confusion sur le paramètre à donner à concrete_name lors du commit 9450	herbelin
2006-12-13	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin
2006-12-12	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin
2006-12-09	Évitement des noms de constructeurs dans les motifs de filtrage de "match"	herbelin
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-06	Déplacement de on_judgment_type de Typeops vers Termops	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-02-07	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin
2006-02-07	Mise en conformité de l'ordre des occurrences de pattern avec l'affichage	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-08-19	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey
2005-05-25	Added subtac contrib.	coq
2005-02-18	Ajout it_mkNamedProd_wo_LetIn	herbelin
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-08-24	Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-03-15	preparation pour release (suite)	barras
2004-02-13	Deplacement array_map_left and co dans Util	herbelin
2003-11-24	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin
2003-10-22	Deplacement de iter_constr_with_full_binders dans Termops	herbelin
2003-10-13	Deplacement next_global_ident_away dans Termops	herbelin
2003-10-02	Le nom '_' n'est plus valable en v8 pour nommer les variables	herbelin
2003-09-23	Changement de l'afficheur pour que les variables liées aient un nom indépen...	herbelin
2003-09-13	Deplacement de Declare vers Termops	herbelin
2003-09-12	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-03-12	* empty log message *	barras
2002-12-23	Prise en compte application partielle dans dependent	herbelin
2002-12-19	Petit netoyage dans lib	coq
2002-11-18	Allègement du noyau	herbelin
2002-10-15	nom de fonction plus simple	barras