aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2005-06-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7098 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-31majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7096 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-31coqwc: Admittedfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7095 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7093 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7091 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7089 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-28unification: evar_define checks the free variables are bound in the evar contextbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7088 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7086 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7084 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26No parentheses around f in 'f \subst{...}'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7083 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Utilisation du module Buffer; encodage plus rigoureux des symboles en uriherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7082 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Correction of a bug in functional scheme. It raised with mutualcoq
functions with imbricated recursive calls. Two bugs in one actually, one in the building of the set of recursive functions, and one with De Bruijn indices when looking for recursve calls. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7080 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Patch to avoid Whelp bug removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7079 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Add a guard for V7 mode, CVS compiles cleanly again :)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7078 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26New environment variable COQREMOTEBROWSER to set the command used by Coqsacerdot
and coqide to control a remote browser. It uses the standard syntax where "%s" is the placeholder for the URL. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7077 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7075 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-25Forgot to remove a cmo.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7074 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-25Added subtac contrib.coq
Added some debug printer in termops. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7071 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-15 04:00:28 +0000