aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2006-12-28Cleaning backtracking code, optimized "Backtrack n x y" when n iscourtieu
2006-12-26Report correction bug #1289 dans trunk (r9435 pour branche v8.1)herbelin
2006-12-23Doc for Combined Scheme.msozeau
2006-12-23Addition of a "Combined Scheme" vernacular command for building the conjuncti...msozeau
2006-12-22Default tactic for solving goals.msozeau
2006-12-22remplacement d'un test d'egalite par un test de convertibilite dans injection...jforest
2006-12-21typo malencontreusefilliatr
2006-12-19Adaptation à Subversion 1.4notin
2006-12-17reparation bug 1239letouzey
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
2006-12-15contrib/dp: tactique ergo (voir ergo.lri.fr)filliatr
2006-12-14Confusion sur le paramètre à donner à concrete_name lors du commit 9450herbelin
2006-12-14Reimplemented equality generation for pattern matching at typing time. First ...msozeau
2006-12-13Alignement de la politique de renommage de rename_bound_var (utilisé pourherbelin
2006-12-13test condition de gardebarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:42:28 +0000