aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* NettoyageGravatar herbelin2000-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@717 85f007b7-540e-0410-9357-904b9bb8a0f7
* globalize_command devient globalize_constrGravatar herbelin2000-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pb de globalisation dans print_mutualGravatar herbelin2000-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@715 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@714 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pb factorisation de Print GrammarGravatar herbelin2000-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@713 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement "command" en "constr" et globalize_command en globalize_constrGravatar herbelin2000-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug affichage des infixGravatar herbelin2000-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ↵Gravatar herbelin2000-10-13
| | | | | | versions exact_no_check, exact_check git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@709 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code redondantGravatar herbelin2000-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@708 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'un test inutile dans RCastGravatar herbelin2000-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code redondantGravatar herbelin2000-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@706 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ↵Gravatar herbelin2000-10-13
| | | | | | versions exact_no_check, exact_check git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@705 85f007b7-540e-0410-9357-904b9bb8a0f7
* TODOGravatar herbelin2000-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@704 85f007b7-540e-0410-9357-904b9bb8a0f7
* ParenthesesGravatar herbelin2000-10-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@703 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hypotheses des ind oubliees dans le dischargeGravatar herbelin2000-10-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Idem pour défs locales dans VarGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@701 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@700 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau type rec_declarationGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des find_m*typeGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@698 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite du précédentGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@697 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delta des défs locales en de Bruijn toujours pas stableGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@696 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout push_rec_typesGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@695 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout mind_arities_envGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des find_m*typeGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'environnement dans le calcul des implicitesGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@692 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'environnement dans les tests de bonne fondaisonGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@691 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'environnement dans les tests de correction des inductifsGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@690 85f007b7-540e-0410-9357-904b9bb8a0f7
* C'était pas le bon env dans build_termGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Niveau d'associativité du letGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de Let à certains endroitsGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)Gravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'env local dans make_apply_entryGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Message d'erreur bad patternGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@684 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage du nom des letinGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans [prvecti v] quand v est videGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@681 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de bugs (alias initiaux et ordre des cas par défaut)Gravatar herbelin2000-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus d'échec sur les globaux lorsque prterm est appelé par le débuggerGravatar herbelin2000-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug ordre dans push_relsGravatar herbelin2000-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement, encore un Simpl inutileGravatar herbelin2000-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Messages d'erreurs CasesGravatar herbelin2000-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@675 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour nouvelle syntaxe des membres droits des grammairesGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@672 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parenthèses pour les tactiquesGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en page de Print HintGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@670 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans la stratégie de réduction du Fix par SimplGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@669 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug splay_prod_assumGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@668 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-29 22:09:55 +0000