aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-06-25eq and eqT are the samebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5825 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25simplified proof (eq and eqT are now the same)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5824 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25correspondance des records et noms de champs de records entre un module et ↵letouzey
sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5822 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5821 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5820 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5819 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5818 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5817 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5816 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-17Nouvelle syntaxe à la ML pour donner le type ML des extensions d'argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5815 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5814 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5813 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5812 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5811 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5810 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5809 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5808 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5807 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5806 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5805 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5804 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5803 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-03Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5802 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5801 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5800 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Amélioration affichage coercions vers Funclassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5799 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Fusion comparaison Const/Var; export is_opaqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5796 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Nouveaux thms de non circularité de natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5795 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02eq2eqT et eqT2eq devenus obsolètesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5794 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Affichage de l'opacité dans Print et Aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5793 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Recherche de la source à partir de la gauche pour gérer des cas comme ↵herbelin
'Coercion plus : nat >-> Funclass' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5791 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02MacOS X dans /usr/localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5790 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02commentaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5789 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Ajout tests affichage coercions vers Funclassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5788 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Ajout testsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5787 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Plus de robustesse en traduisant les 'Repeat Induction' et les 'Do n Induction'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5786 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02bug #787 de Rolandbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5783 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Clarify the distinction between quantified_hypothesis and ↵herbelin
declared_or_quantified_hypothesis; fixed the interpretation of the hyp in with-bindings, intro until, simple destruct and simple induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5782 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02MAJ docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5779 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5778 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5777 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5776 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5775 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-28Retour sur amendement de l'interprétation mult sur nat (bug 743) car ↵herbelin
incompatible avec la sémantique précédente qui identifiait "Z_of_nat x * Z_of_nat y" avec "Z_of_nat (x * y)" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5774 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5772 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-27Bug affichage ClearBodyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5771 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-27Bricoles (cf bug #782)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5769 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-27Un bug résiduel (mais pas bien méchant) du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5767 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5765 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 18:38:38 +0000