coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye	2001-10-23
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin	2001-10-17
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
*	Incompatibilité entre la prise en compte des univers au niveau des tactiques...	herbelin	2001-10-10
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Petit oubli à propos de ThinBody	herbelin	2001-10-05
*	Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...	herbelin	2001-10-05
*	Ajout de dynamiques pour les quotations constr et tactic	delahaye	2001-10-02
*	Ajout du printer de tactiques + modif du Dynamic ocaml	delahaye	2001-09-30
*	Changement du message d'erreur pour l'interpreteur de tactiques	delahaye	2001-09-24
*	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