aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2006-11-20Correction boucle du parseur en cas de caractÃère non unicodeherbelin
2006-11-20Suppression du type 'tac dans les abstract_argument_type: devenu inutile herbelin
2006-11-19Dépendance inutile en Tacexpr, de proofs, qui se compile en principe aprèsherbelin
2006-11-19mult_sym, plus_sym -> mult_comm, plus_commherbelin
2006-11-19MAJherbelin
2006-11-19Raffinement de l'unification de "apply": mémorisation de certainsherbelin
2006-11-18Code mort (duplication de code dans reductionops.ml)herbelin
2006-11-17The emacs-U option now does not output *any* char above 250.courtieu
2006-11-16Small fix in functional graph merging.courtieu
2006-11-16suppression de code mort (avec bug de nom)letouzey
2006-11-16pb avec r9379 + modifs dans ringbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 19:15:02 +0000