aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2007-01-11Petit oubli dans commit 9474herbelin
2007-01-11Ajout d'une option de débogage pour expliciter l'instance des evarsherbelin
2007-01-10 - Make .vo files depend on coqdoc if COQ_XML is set (bug #848)lmamane
2007-01-10Merge with Lionel Elie Mamane's private branch:lmamane
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
2007-01-10Suite commit restructuration discharge (application du type deherbelin
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2007-01-08Subtac fixes, support for reasoning on wf defs.msozeau
2007-01-05suite de la reparation du bug 1239: apres les inds, les records et vars de typesletouzey
2007-01-02Rework subtac pattern matching equalities generation.msozeau
2007-01-02Add f_equal case for 6 arguments.msozeau
2006-12-29Protection contre une source possible de liaison de lambda anonymeherbelin
2006-12-28Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àherbelin
2006-12-28Correction petits bugs du check de la test-suiteherbelin
2006-12-28Remplacement de la définition de Pind et Prec par une définitionherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 12:16:13 +0000