coq - The formal proof system

Age	Commit message (Expand)	Author
2001-11-12	Suppression des stamps et donc des *_constraints	clrenard
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-06	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-10-23	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-10-10	Incompatibilité entre la prise en compte des univers au niveau des tactiques...	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-10-05	Petit oubli à propos de ThinBody	herbelin
2001-10-05	Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...	herbelin
2001-10-02	Ajout de dynamiques pour les quotations constr et tactic	delahaye
2001-09-30	Ajout du printer de tactiques + modif du Dynamic ocaml	delahaye
2001-09-24	Changement du message d'erreur pour l'interpreteur de tactiques	delahaye
2001-09-21	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-20	Transparent	barras
2001-09-17	unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec les	barras
2001-09-14	exceptions	barras
2001-09-10	Un conv aurait dû être un conv_leq	herbelin
2001-09-09	Nettoyage reduce_to_ind et one_step_reduce	herbelin
2001-09-09	Suppression du retypage dans w_Declare	herbelin
2001-08-10	Parsing	herbelin
2001-08-08	Ajout nf_betaiota dans le cut interne	herbelin
2001-08-07	Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...	herbelin
2001-08-05	Code mort	herbelin
2001-07-24	Suppression de l'affichage du non-reparsable 'Local constraint change'	herbelin
2001-07-19	Changements dans le traitement des qualid's	delahaye
2001-07-02	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-06-29	Autoriser Apply avec un but sous forme d'implication ou de quantification	barras
2001-06-29	Backtracking pour le Match	delahaye
2001-06-25	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin
2001-06-19	Extension des parametres de Clear + Inst	delahaye
2001-06-18	Interpretation MetaId + Progress + Inst	delahaye
2001-05-28	Pretty -> Prettyp	filliatr
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-18	Erreur dans un commentaire ...	clrenard
2001-05-07	quelques bug reports mineurs	barras
2001-05-03	Changement de la structure des points fixes	barras
2001-04-19	Metas dans les Unfold's	delahaye
2001-04-14	Reparation du bug de Try	delahaye
2001-04-12	Ajout de _ dans les patterns d'intro	mohring
2001-04-03	utilisation de Options.if_verbose	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2001-03-05	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-03-01	backtrack unification types et deplacement make_clenv_binding	filliatr