aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2006-12-13svn:ignoreherbelin
2006-12-13Dépliage du terme d'induction avant suppression quand celui-ci est unherbelin
2006-12-12Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...notin
2006-12-12Correction du bug #1273 (problème avec les paramètres non récursivement un...notin
2006-12-12Subtac: work on cases.msozeau
2006-12-12nouvelle indentation des scriptsbarras
2006-12-12cosmetiquebarras
2006-12-12Variable print_instances pour déboguer les instances d'evarherbelin
2006-12-12Dépendence inutileherbelin
2006-12-12AllÃègement de syntxe suite à l'introduction de l'unif patternherbelin
2006-12-12Bug nommage Zgt_trans_succherbelin
2006-12-12Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...herbelin
2006-12-12MAJherbelin
2006-12-12Test bug #932herbelin
2006-12-12Correction bug #1041 (double cause : non évitement des noms existants enherbelin
2006-12-11correction Open Local Scope (Ring)bgregoir
2006-12-11Changement dans le kernel : bgregoir
2006-12-09Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)herbelin
2006-12-09Évitement des noms de constructeurs dans les motifs de filtrage de "match"herbelin
2006-12-09git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9423 85f007b7-540e-04...filliatr
2006-12-08bug condition de gardebarras
2006-12-08dpfilliatr
2006-12-08contrib/dpfilliatr
2006-12-08Pas d'escamotage des noms réservés si Set Printing All actibvéherbelin
2006-12-08Suite ajout option -output-contextherbelin
2006-12-08git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 85f007b7-540e-04...filliatr
2006-12-08Ajout d'une option -output-context qui affiche le contexte en CCI pur à laherbelin
2006-12-08Correction typo règle réduction du fix chapitre CCIherbelin
2006-12-08Subtac bug fix, add list take example.msozeau
2006-12-03MAJherbelin
2006-12-03Remplacement de la dépendance de G_vernac en G_constr (sourceherbelin
2006-12-01add a comment about Show Existentials and a question about case_eq jnarboux
2006-11-29Fork of cases impl for subtac.msozeau
2006-11-29correction du bug : VM value extraction error (PR#1290)bgregoir
2006-11-27The $(BEST) binaries symlinks depend on existence of target, not newness.lmamane
2006-11-24Functional graph merging deals with letins.courtieu
2006-11-24Fixed the graph merging parameter order.courtieu
2006-11-24Fixed the -emacs option which was always On.courtieu
2006-11-23Fixing syntax and parameter order in functional graph merging.courtieu
2006-11-22Code mort découvert par Matthieuherbelin
2006-11-21Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deherbelin
2006-11-21un caractere blanc parasite dans svn:ignoreletouzey
2006-11-20Changing merging functional scheme syntax.courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 22:48:41 +0000