aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* modif test constGravatar mayero2001-09-18
* Blindage de Show IntroGravatar letouzey2001-09-17
* unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec lesGravatar barras2001-09-17
* quotation des noms de fichiers pour eviter une mauvaise interpretation des \Gravatar barras2001-09-17
* MAJGravatar herbelin2001-09-14
* Search prenait en compte le contenu des sections alors que celui-ci n'existe ...Gravatar herbelin2001-09-14
* MAJ vis à vis de la nouvelle non-localité des Remark/FactGravatar herbelin2001-09-14
* Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)Gravatar herbelin2001-09-14
* Transformation de Remark/Fact en constantes non visibles sans qualificationGravatar herbelin2001-09-14
* Ajout syntaxe "Assert H:T."Gravatar herbelin2001-09-14
* L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...Gravatar herbelin2001-09-14
* L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...Gravatar herbelin2001-09-14
* exceptionsGravatar barras2001-09-14
* mauvais rattrapage d'exceptionGravatar barras2001-09-14
* Only CHANGES !Gravatar herbelin2001-09-13
* Structuration et traductionGravatar herbelin2001-09-13
* Prise en compte qualid dans Hint UnfoldGravatar herbelin2001-09-13
* Syntaxe des HintsGravatar herbelin2001-09-13
* uniformité des cibles pour les contribsGravatar filliatr2001-09-13
* mise à jourGravatar filliatr2001-09-13
* eclaircissement du codeGravatar courant2001-09-13
* explications modifications TautoGravatar courant2001-09-13
* *** empty log message ***Gravatar mohring2001-09-12
* Rustine pour gérer inject_natGravatar herbelin2001-09-12
* Un look un peu plus avenant aux productions des règles de grammaireGravatar herbelin2001-09-11
* Du bon usage des commentaires coqwebGravatar herbelin2001-09-11
* Conformité des commentaires au format coqwebGravatar herbelin2001-09-11
* MAJGravatar herbelin2001-09-11
* Hack pour gérer les univers dans les prédicats de Cases synthétisésGravatar herbelin2001-09-10
* changement du make depend en vu du make realsGravatar letouzey2001-09-10
* bug de rename_global modulaire corrige'Gravatar letouzey2001-09-10
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10
* Un conv aurait dû être un conv_leqGravatar herbelin2001-09-10
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10
* Légère modification lookup_eliminatorGravatar herbelin2001-09-09
* Nettoyage reduce_to_ind et one_step_reduceGravatar herbelin2001-09-09
* Passage aux univers algébriquesGravatar herbelin2001-09-09
* Passage aux univers algébriquesGravatar herbelin2001-09-09
* Amélioration check_module_nameGravatar herbelin2001-09-09
* Préparation à la mise en place d'univers algébriquesGravatar herbelin2001-09-09
* Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...Gravatar herbelin2001-09-09
* Préparation du prétypage à la mise en place d'univers algébriquesGravatar herbelin2001-09-09
* Mécanisme pour faire remonter les contraintes de typage sur les variables de...Gravatar herbelin2001-09-09
* Mécanisme pour faire remonter les contraintes de typage sur les variables de...Gravatar herbelin2001-09-09
* Suppression du retypage dans w_DeclareGravatar herbelin2001-09-09
* MAJGravatar herbelin2001-09-09
* Tests l'incohérence des universGravatar herbelin2001-09-09
* MAJGravatar herbelin2001-09-08
* MAJGravatar herbelin2001-09-07
* Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)Gravatar herbelin2001-09-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 16:17:31 +0000