coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Let doit etre utilise dans le mode de preuve	delahaye	2001-01-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1233 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rattrapage d'erreur pour le Case + Eval Compute in pour Definition	delahaye	2001-01-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1232 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du Let pour le langage de tactiques	delahaye	2000-12-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Améliorations	herbelin	2000-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1230 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug installation non locale	herbelin	2000-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1228 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1227 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Dernière MAJ	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1226 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1225 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug de contextes	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1224 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1223 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Elimination des coupures	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1222 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement du type stack de Reduction vers Closure et utilisation pour ↵	herbelin	2000-12-26
\| \| \| \| \| \|	accélérer la réduction dans Closure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1221 85f007b7-540e-0410-9357-904b9bb8a0f7
*	On n'évite plus les globaux dans Intro, mais on les évite dans Abstract	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1220 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pattern sera mieux dans Pretyping; relâchement head_pattern_bound	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1219 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce ↵	herbelin	2000-12-26
\| \| \| \| \| \|	dernier qui échouera si c'est pas normalisé de tête git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1218 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1217 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Command -> Constr	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1216 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retrait du test d'existence "is_global" dans Intro ( fresh_id ) d	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1215 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Normalisation betaiota du pattern avant enregistrement comme hint (certains ↵	herbelin	2000-12-25
\| \| \| \| \| \|	développements exploite cette caractéristique) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1214 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug head_pattern_bound	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1213 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modifs sur le langage de tactiques et pas de "ë" dans Micaela	delahaye	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1212 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Langage de tactiques, AutoRewrite, Tauto-Intuition + autres modifs	delahaye	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug confusion existS/sigS	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1210 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Token n'est plus un keyword	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1209 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Command -> Constr	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1208 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1207 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de debug en assert	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1206 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug discharge process_class	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1205 85f007b7-540e-0410-9357-904b9bb8a0f7
*	find_section_variable : un traducteur id -> sp pour variables de section; ↵	herbelin	2000-12-25
\| \| \| \| \| \|	variable_strength change de type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1204 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Alias variable_path	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1203 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Effet réorganisation Classops	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1202 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un nom long pour les variables de section qui font classe ou coercion; ↵	herbelin	2000-12-25
\| \| \| \| \| \|	réorganisation; bugs discharge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1201 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug vieux Match	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1200 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug prédicat	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1199 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traducteur automatique de scripts vernac	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1198 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mayero	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1197 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1196 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1195 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cleanall	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1194 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Insertion COQPATHPREFIX pour isntallation locale	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1193 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oublis	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1192 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ V7	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1191 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mauvais numéro de version de camlp4 requis	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1190 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour créer les archives distribuées	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1189 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Novembre -> Décembre	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1188 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Création...	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1187 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1186 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction en francais de 'CHANGES' dont le contenu était en français	herbelin	2000-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Re-MAJ	herbelin	2000-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1184 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1183 85f007b7-540e-0410-9357-904b9bb8a0f7