coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	* Fixed constr_cmp again to handle universes subtyping correctly	puech	2008-10-09
*	Fixing constr_cmp, propagating subtyping only right of a product	puech	2008-10-02
*	Fix a bug, in fold_constr_with_binders, the types of fixpoints were	msozeau	2008-09-13
*	Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par	herbelin	2008-08-04
*	Backport r11289.	msozeau	2008-07-29
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	Correction bug 1878 (utilisation de extend_evar déplacée là où une	herbelin	2008-06-14
*	Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".	herbelin	2008-06-11
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...	barras	2008-05-28
*	Changement de stratégie vis à vis du commit 10859 sur la gestion des	herbelin	2008-05-12
*	- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des	herbelin	2008-05-10
*	Réutilisation de l'infrastructure pour le polymorphisme d'univers des	herbelin	2008-04-30
*	Petites corrections vis à vis des commits 10860, 10859, 10850	herbelin	2008-04-28
*	Correction du bug des types singletons pas sous-type de Set	herbelin	2008-04-27
*	* Factorizing code : context_chop was used in several files (even as chop_con...	vsiles	2008-03-17
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
*	- Ajout de la possibilité d'utiliser la notation Record pour les	herbelin	2007-06-30
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	Confusion sur le paramètre à donner à concrete_name lors du commit 9450	herbelin	2006-12-14
*	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin	2006-12-13
*	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin	2006-12-12
*	Évitement des noms de constructeurs dans les motifs de filtrage de "match"	herbelin	2006-12-09
*	Compatibilité du polymorphisme de constantes avec les sections.	herbelin	2006-10-29
*	Déplacement de on_judgment_type de Typeops vers Termops	herbelin	2006-10-06
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	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	2006-02-07
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey	2005-08-19
*	Added subtac contrib.	coq	2005-05-25
*	Ajout it_mkNamedProd_wo_LetIn	herbelin	2005-02-18
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)	herbelin	2004-08-24
*	Nouvelle en-tête	herbelin	2004-07-16
*	preparation pour release (suite)	barras	2004-03-15
*	Deplacement array_map_left and co dans Util	herbelin	2004-02-13
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Deplacement de iter_constr_with_full_binders dans Termops	herbelin	2003-10-22
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
*	Le nom '_' n'est plus valable en v8 pour nommer les variables	herbelin	2003-10-02