aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-09-18modif test constmayero
2001-09-17Blindage de Show Introletouzey
2001-09-17unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec lesbarras
2001-09-17quotation des noms de fichiers pour eviter une mauvaise interpretation des \barras
2001-09-14MAJherbelin
2001-09-14Search prenait en compte le contenu des sections alors que celui-ci n'existe ...herbelin
2001-09-14MAJ vis à vis de la nouvelle non-localité des Remark/Factherbelin
2001-09-14Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)herbelin
2001-09-14Transformation de Remark/Fact en constantes non visibles sans qualificationherbelin
2001-09-14Ajout syntaxe "Assert H:T."herbelin
2001-09-14L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...herbelin
2001-09-14L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...herbelin
2001-09-14exceptionsbarras
2001-09-14mauvais rattrapage d'exceptionbarras
2001-09-13Only CHANGES !herbelin
2001-09-13Structuration et traductionherbelin
2001-09-13Prise en compte qualid dans Hint Unfoldherbelin
2001-09-13Syntaxe des Hintsherbelin
2001-09-13uniformité des cibles pour les contribsfilliatr
2001-09-13mise à jourfilliatr
2001-09-13eclaircissement du codecourant
2001-09-13explications modifications Tautocourant
2001-09-12*** empty log message ***mohring
2001-09-12Rustine pour gérer inject_natherbelin
2001-09-11Un look un peu plus avenant aux productions des règles de grammaireherbelin
2001-09-11Du bon usage des commentaires coqwebherbelin
2001-09-11Conformité des commentaires au format coqwebherbelin
2001-09-11MAJherbelin
2001-09-10Hack pour gérer les univers dans les prédicats de Cases synthétisésherbelin
2001-09-10changement du make depend en vu du make realsletouzey
2001-09-10bug de rename_global modulaire corrige'letouzey
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-09-10Un conv aurait dû être un conv_leqherbelin
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-09-09Légère modification lookup_eliminatorherbelin
2001-09-09Nettoyage reduce_to_ind et one_step_reduceherbelin
2001-09-09Passage aux univers algébriquesherbelin
2001-09-09Passage aux univers algébriquesherbelin
2001-09-09Amélioration check_module_nameherbelin
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
2001-09-09Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...herbelin
2001-09-09Préparation du prétypage à la mise en place d'univers algébriquesherbelin
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables de...herbelin
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables de...herbelin
2001-09-09Suppression du retypage dans w_Declareherbelin
2001-09-09MAJherbelin
2001-09-09Tests l'incohérence des universherbelin
2001-09-08MAJherbelin
2001-09-07MAJherbelin
2001-09-07Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-08 17:06:51 +0000