aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-06-09dp: traitement des fixpointscoq
2005-06-09backtrack sur le typage des instantiations d\'evarsbarras
2005-06-08majcoq
2005-06-08traitement des casecoq
2005-06-08evar declarees avec mauvais typebarras
2005-06-07majcoq
2005-06-07majcoq
2005-06-07pas de filtrages partielsbarras
2005-06-07reparations de quelques petits bugs d\'unification + introduction de la notio...barras
2005-06-06majcoq
2005-06-06essai de typage des instantiations d\'evarsbarras
2005-06-05majcoq
2005-06-05majcoq
2005-06-05eradication de Evarutil.w_Definebarras
2005-06-05assouplissement de real_clean: ne tient pas compte des occcurences flexibles ...barras
2005-06-04majcoq
2005-06-04Ajout explicite du niveau 200 de pattern auquel on fait référence au niveau...herbelin
2005-06-03majcoq
2005-06-03Prise en compte de l'utilisation des notations récursives pour faire une not...herbelin
2005-06-03suppression de code commentecoq
2005-06-03whelp + correction bug affichage de coqidecoq
2005-06-02majcoq
2005-06-01majcoq
2005-05-31majcoq
2005-05-31coqwc: Admittedfilliatr
2005-05-30majcoq
2005-05-29majcoq
2005-05-28majcoq
2005-05-28unification: evar_define checks the free variables are bound in the evar contextbarras
2005-05-27majcoq
2005-05-26majcoq
2005-05-26No parentheses around f in 'f \subst{...}'herbelin
2005-05-26Utilisation du module Buffer; encodage plus rigoureux des symboles en uriherbelin
2005-05-26Correction of a bug in functional scheme. It raised with mutualcoq
2005-05-26Patch to avoid Whelp bug removed.sacerdot
2005-05-26Add a guard for V7 mode, CVS compiles cleanly again :)coq
2005-05-26New environment variable COQREMOTEBROWSER to set the command used by Coqsacerdot
2005-05-25majcoq
2005-05-25Forgot to remove a cmo.coq
2005-05-25Added subtac contrib.coq
2005-05-24majcoq
2005-05-24majcoq
2005-05-24Added clenv_environments_evars that behaves as clen_environments butsacerdot
2005-05-24New commit to allow definitions of morphisms on relations whose carrier issacerdot
2005-05-24WARNING: unification changed (to fix a bug).sacerdot
2005-05-24dp: ajout du prouveur Zenoncoq
2005-05-23majcoq
2005-05-23Consequence of allowing the numerical argument of auto to be an ident for ltacherbelin
2005-05-23Bug fix for a bug reported by Roland: the function that detects the constantssacerdot
2005-05-22majcoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 09:34:18 +0000