aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-10-11MAJherbelin
2000-10-11Nouveau type rec_declarationherbelin
2000-10-11Renommage des find_m*typeherbelin
2000-10-11Suite du précédentherbelin
2000-10-11Delta des défs locales en de Bruijn toujours pas stableherbelin
2000-10-11Ajout push_rec_typesherbelin
2000-10-11Ajout mind_arities_envherbelin
2000-10-11Renommage des find_m*typeherbelin
2000-10-11Prise en compte de l'environnement dans le calcul des implicitesherbelin
2000-10-11Prise en compte de l'environnement dans les tests de bonne fondaisonherbelin
2000-10-11Prise en compte de l'environnement dans les tests de correction des inductifsherbelin
2000-10-11C'était pas le bon env dans build_termherbelin
2000-10-11Niveau d'associativité du letherbelin
2000-10-11Prise en compte de Let à certains endroitsherbelin
2000-10-11Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)herbelin
2000-10-11Prise en compte de l'env local dans make_apply_entryherbelin
2000-10-11Message d'erreur bad patternherbelin
2000-10-11Prise en compte de Let dans build_dependent_inductiveherbelin
2000-10-11Bug affichage du nom des letinherbelin
2000-10-11Bug dans [prvecti v] quand v est videherbelin
2000-10-10MAJherbelin
2000-10-10Correction de bugs (alias initiaux et ordre des cas par défaut)herbelin
2000-10-10Plus d'échec sur les globaux lorsque prterm est appelé par le débuggerherbelin
2000-10-10Bug ordre dans push_relsherbelin
2000-10-10Finalement, encore un Simpl inutileherbelin
2000-10-10Messages d'erreurs Casesherbelin
2000-10-06MAJherbelin
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
2000-10-06MAJ pour nouvelle syntaxe des membres droits des grammairesherbelin
2000-10-06Parenthèses pour les tactiquesherbelin
2000-10-06Mise en page de Print Hintherbelin
2000-10-06Changement dans la stratégie de réduction du Fix par Simplherbelin
2000-10-06Bug splay_prod_assumherbelin
2000-10-06MAJherbelin
2000-10-06MAJ pr_uniherbelin
2000-10-06Un usage en moins de l'axiome eq_rec_eqherbelin
2000-10-06correction bug univers (dummy_univ)filliatr
2000-10-05Code mort (2ème)herbelin
2000-10-05Code mortherbelin
2000-10-05Bugs de la réduction de Fix dans Simplherbelin
2000-10-05Suppression d'un Cast inutileherbelin
2000-10-05Remplacement de la tactique Program (partiel)herbelin
2000-10-05Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALISTherbelin
2000-10-05Bug de conflit de nommage d'hyp d'induction dans l'Induction fonctionnant dan...herbelin
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs locales (2ème)herbelin
2000-10-04Commit malencontreux sur précédente versionherbelin
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
2000-10-04Nouvelle stratégie de nommage dans Simpl pour Fixherbelin
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs localesherbelin
2000-10-04Code mortherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 09:47:13 +0000