aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-06-30updated printing of evar context (may loop ?)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30instantiate entry: constr -> lconstrcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5856 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5855 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5854 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29Essai de suppression de eta dans simpl (cf bug #779)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5853 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29moved instantiate binding to extratacticscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29License de contrib/interfaceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5849 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29efficacite du lexeurfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5847 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5846 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5845 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28contrib/interface *$*$@!corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5844 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28more evar stuffcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Ajout de la coercion id dans context vers evaluable constant (bug #777)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5841 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Correction bug #776herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5839 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Double bug d'affichage des cases dépendants (bug #784)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5837 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Modules et Records: gros changements pour prendre en compte le nouveau ↵letouzey
mind_record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5836 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5835 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5834 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-27Typo (bug #797)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5832 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-27Correction affichage v8 des records avec let (bug #798)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5830 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-26Licence changed from GPL to Lesser GPL.sacerdot
DTDs licence is still GPL. This should create no problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5828 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-26effective evar refiningcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5827 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5826 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 20:27:27 +0000