aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-01-31Fix order of wf and measure arguments, patch Program doc.msozeau
2007-01-30Nouvelle implantation de clear_hypsnotin
2007-01-30suite du commit 9557 soubiran
2007-01-30Petite correction sur un message d'erreur renvoyé au sous typage.soubiran
2007-01-30constr_of_pat bug with nested patterns.msozeau
2007-01-29bugfix for suffices (support for open head)corbinea
2007-01-29Various fixes in subtac, update some test cases.msozeau
2007-01-29finalized sufficescorbinea
2007-01-29Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.msozeau
2007-01-28"suffices" implemented + syntax cleanupcorbinea
2007-01-28Pas de solution à court terme pour ce problème de complexitéherbelin
2007-01-26Explication du intros until nnotin
2007-01-26Contounement d'un probleme avec la VM dans Function jforest
2007-01-26correction d'un bug d'efficacite dans le printerjforest
2007-01-25decl mode: anonymous factscorbinea
2007-01-25Redondance erronée dans les testsherbelin
2007-01-24doc de ringbgregoir
2007-01-24modifications des messages d'erreurs renvoyés lors de la comparaison soubiran
2007-01-24Update some tests and fix section bug.msozeau
2007-01-24changement de la fonction norm_substbgregoir
2007-01-24Tentative amélioration messages d'erreur prédicat d'élimination (cf notammentherbelin
2007-01-24Correction bug #1333 (test non récursivité des dépendances en d'autresherbelin
2007-01-23Updated Makefile to include ConstructiveEpsilon.vemakarov
2007-01-23Derivation of (exists x : A, P x) -> {x : A | P x} for decidable Pemakarov
2007-01-23ring : Correction du bug PR#1306bgregoir
2007-01-22Correction du bug #1315:notin
2007-01-22Correction d'un bug d'unification-pattern dans l'algo d'unificationherbelin
2007-01-22Allègement de l'affichage des références par le printer si possibleherbelin
2007-01-22Clarification redondance Axiome du choix unique/descriptionherbelin
2007-01-22changes in declarative language : by term using tacticcorbinea
2007-01-22Correction pour le rapport de bug #1325 par rétablissement duherbelin
2007-01-22Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouentherbelin
2007-01-19Prise en compte des univers algébriques dans les types inférés dansherbelin
2007-01-19Export de l'afficheur de substitutions de noms de modules pour le débogueurherbelin
2007-01-19Protection contre les warnings 'unused variable' de ocaml 3.09herbelin
2007-01-19Protection contre les warnings 'unused variable' de ocaml 3.09herbelin
2007-01-19Tests de référence circulaire au sous-typage de module (pour mémoire)herbelin
2007-01-18Update installation instructions to the modern world a bit.lmamane
2007-01-18Update for v8.1lmamane
2007-01-17Move definition of VO_TOOLS_DEP before first use of it.lmamane
2007-01-17Reintroduce compatibility with old versions of GNU makelmamane
2007-01-17Correction bug #1282herbelin
2007-01-17Correction bug #1302herbelin
2007-01-17Correction adresse CoRN dans FAQ (suite)herbelin
2007-01-17Correction adresse CoRN dans FAQ (cf #1317)herbelin
2007-01-17README update:lmamane
2007-01-15Various subtac fixes.msozeau
2007-01-12Suite au mail de Lionel a propos du Makefile: letouzey
2007-01-12un saut de ligne ...letouzey
2007-01-12addition du neq unicodeletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-07 04:38:26 +0000