aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-06-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7178 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-28Correction bug #983herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7176 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7174 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7172 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7170 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7168 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7167 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-24Dp: ajout d'abstraction aux applications de fonction non premier ordrecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7166 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-24dp: ajout des prédicats de sortescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7165 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7163 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-22Added entry constr_may_eval for tactic extensions (new syntax)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7162 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7160 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-21coqdep connait maintenant user-contribfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7158 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7156 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7154 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7152 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7150 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7148 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7146 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7145 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-15Dp : ajoût des existentielscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7144 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7142 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7140 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7138 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7136 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7134 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7132 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7131 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-09dp: traitement des fixpointscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7130 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-09backtrack sur le typage des instantiations d\'evarsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7129 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7127 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-08traitement des casecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7126 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-08evar declarees avec mauvais typebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7125 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7123 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7122 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07pas de filtrages partielsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7121 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07reparations de quelques petits bugs d\'unification + introduction de la ↵barras
notion de variable de sortes (mais pas encore utilise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7120 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7118 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-06essai de typage des instantiations d\'evarsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7115 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7114 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05eradication de Evarutil.w_Definebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7113 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05assouplissement de real_clean: ne tient pas compte des occcurences flexibles ↵barras
des variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7112 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7110 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-04Ajout explicite du niveau 200 de pattern auquel on fait référence au ↵herbelin
niveau 0; nécessaire pour option -nois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7109 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7105 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03Prise en compte de l'utilisation des notations récursives pour faire une ↵herbelin
notation alternative de l'application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7104 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03suppression de code commentecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7103 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03whelp + correction bug affichage de coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7102 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7100 85f007b7-540e-0410-9357-904b9bb8a0f7