coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction due au changement de semantique de Match	delahaye	2001-09-21
*	Problème d'affichage d'un . pour les Local_constraints; remplacement par Idtac	herbelin	2001-09-21
*	Transparent	barras	2001-09-20
*	unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec les	barras	2001-09-17
*	exceptions	barras	2001-09-14
*	Un conv aurait dû être un conv_leq	herbelin	2001-09-10
*	Nettoyage reduce_to_ind et one_step_reduce	herbelin	2001-09-09
*	Suppression du retypage dans w_Declare	herbelin	2001-09-09
*	Parsing	herbelin	2001-08-10
*	Ajout nf_betaiota dans le cut interne	herbelin	2001-08-08
*	Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...	herbelin	2001-08-07
*	Code mort	herbelin	2001-08-05
*	Suppression de l'affichage du non-reparsable 'Local constraint change'	herbelin	2001-07-24
*	Changements dans le traitement des qualid's	delahaye	2001-07-19
*	Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...	herbelin	2001-07-02
*	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin	2001-07-02
*	Autoriser Apply avec un but sous forme d'implication ou de quantification	barras	2001-06-29
*	Backtracking pour le Match	delahaye	2001-06-29
*	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin	2001-06-25
*	Extension des parametres de Clear + Inst	delahaye	2001-06-19
*	Interpretation MetaId + Progress + Inst	delahaye	2001-06-18
*	Pretty -> Prettyp	filliatr	2001-05-28
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Erreur dans un commentaire ...	clrenard	2001-05-18
*	quelques bug reports mineurs	barras	2001-05-07
*	Changement de la structure des points fixes	barras	2001-05-03
*	Metas dans les Unfold's	delahaye	2001-04-19
*	Reparation du bug de Try	delahaye	2001-04-14
*	Ajout de _ dans les patterns d'intro	mohring	2001-04-12
*	utilisation de Options.if_verbose	filliatr	2001-04-03
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr	2001-03-05
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	backtrack unification types et deplacement make_clenv_binding	filliatr	2001-03-01
*	introduction d'un refine avec resolution des types et de l'instantiation des ...	mohring	2001-02-28
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
*	Prise en compte noms longs dans SuperAuto	herbelin	2001-02-16
*	Obsolète (cf Coqlib)	herbelin	2001-02-14
*	simplification du make depend; fonctions de stat. util. memoire dans certains...	filliatr	2001-02-08
*	exporting traverse_to and mutate: they are used in pcoq.	bertot	2001-02-08
*	Reparation du pretty-print pour les tactiques	delahaye	2001-02-07
*	Correction pour les Unfold/Fold dans Cbv	delahaye	2001-02-06
*	application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés	filliatr	2001-02-01
*	* empty log message *	mohring	2001-02-01
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	make doc	herbelin	2001-01-27
*	Retour en arrière sur le pb f_equal en attente meilleure solution	herbelin	2001-01-22
*	Bug « f_equal » : arguments inférables par une unification des types qui n...	herbelin	2001-01-21
*	Meta Definition + Tactic Definition	delahaye	2001-01-09