aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-05-14test de conversion laissait echapper exception NotConvertiblebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5746 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5745 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-13"comments only" commit.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5744 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5743 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5742 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5739 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5738 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-08un argument booleen inutilisé dans expand_macrosletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5737 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5736 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-07Bug mauvais sigmaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5735 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-07Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est ↵herbelin
de toutes façons inutile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5733 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5732 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5730 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5729 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5728 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-04Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5726 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5724 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-03but autoamtics tactics savingmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5723 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-03Points-fixes avec let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5722 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5721 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-02Ajout test bug 711herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5720 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5719 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-30Achèvement du passage des emprunts à cameleon de Maxence Guesdon de la ↵herbelin
version 1.2 (QPL) à la version 1.3 (GPL) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5717 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-30Terminologie plus intuitive: evaluable -> unfoldableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5716 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-30Dépendance en $(RPMTOPDIR)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5715 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-30Position du %defattr importanteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5714 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5713 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-29Test bug 705herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5712 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-29Prise en compte d'un type dont la sorte est une evarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5710 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5709 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-28Ajout test If nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5708 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5707 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-27Correction incapacité à gérer les annotations de type dépendantes pour ↵herbelin
le if-then-else git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5706 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5702 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5701 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5700 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5699 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5698 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5696 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-21pb install de pcoqbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5695 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5694 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5693 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20amelioration des specs RPMbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5692 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20Amélioration message d'erreur quand échec unificationclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5691 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20maj annonce depuis la v8beta vers v8narboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5690 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5689 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5688 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17Incorrection exportation XMLherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5687 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17Finalement pas de liste des contributions (cela n'avait été fait que pour ↵herbelin
la 7.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5686 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17pb facto des Fixpoint + erreur avec -dump-glob et Loadbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 85f007b7-540e-0410-9357-904b9bb8a0f7