aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-10-11Idem pour défs locales dans Varherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@701 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@700 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Nouveau type rec_declarationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@699 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Renommage des find_m*typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@698 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Suite du précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@697 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Delta des défs locales en de Bruijn toujours pas stableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@696 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Ajout push_rec_typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@695 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Ajout mind_arities_envherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@694 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Renommage des find_m*typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@693 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de l'environnement dans le calcul des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@692 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de l'environnement dans les tests de bonne fondaisonherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@691 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de l'environnement dans les tests de correction des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@690 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11C'était pas le bon env dans build_termherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@689 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Niveau d'associativité du letherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@688 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de Let à certains endroitsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@687 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@686 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de l'env local dans make_apply_entryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@685 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Message d'erreur bad patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@684 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Prise en compte de Let dans build_dependent_inductiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@683 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Bug affichage du nom des letinherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@682 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Bug dans [prvecti v] quand v est videherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@681 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-10MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@680 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-10Correction de bugs (alias initiaux et ordre des cas par défaut)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@679 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-10Plus d'échec sur les globaux lorsque prterm est appelé par le débuggerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@678 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-10Bug ordre dans push_relsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@677 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-10Finalement, encore un Simpl inutileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@676 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-10Messages d'erreurs Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@675 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@674 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06MAJ pour nouvelle syntaxe des membres droits des grammairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@672 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Parenthèses pour les tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@671 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Mise en page de Print Hintherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@670 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Changement dans la stratégie de réduction du Fix par Simplherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@669 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Bug splay_prod_assumherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@668 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@667 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06MAJ pr_uniherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@666 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Un usage en moins de l'axiome eq_rec_eqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@665 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06correction bug univers (dummy_univ)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@664 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Code mort (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@663 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@662 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Bugs de la réduction de Fix dans Simplherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@661 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Suppression d'un Cast inutileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@660 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Remplacement de la tactique Program (partiel)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@659 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALISTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@658 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Bug de conflit de nommage d'hyp d'induction dans l'Induction fonctionnant ↵herbelin
dans les hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@657 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs locales (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@656 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Commit malencontreux sur précédente versionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@655 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@654 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Nouvelle stratégie de nommage dans Simpl pour Fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@653 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@652 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 12:38:59 +0000