aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...Gravatar herbelin2006-12-12
* MAJGravatar herbelin2006-12-12
* Test bug #932Gravatar herbelin2006-12-12
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* correction Open Local Scope (Ring)Gravatar bgregoir2006-12-11
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)Gravatar herbelin2006-12-09
* Évitement des noms de constructeurs dans les motifs de filtrage de "match"Gravatar herbelin2006-12-09
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9423 85f007b7-540e-04...Gravatar filliatr2006-12-09
* bug condition de gardeGravatar barras2006-12-08
* dpGravatar filliatr2006-12-08
* contrib/dpGravatar filliatr2006-12-08
* Pas d'escamotage des noms réservés si Set Printing All actibvéGravatar herbelin2006-12-08
* Suite ajout option -output-contextGravatar herbelin2006-12-08
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 85f007b7-540e-04...Gravatar filliatr2006-12-08
* Ajout d'une option -output-context qui affiche le contexte en CCI pur à laGravatar herbelin2006-12-08
* Correction typo règle réduction du fix chapitre CCIGravatar herbelin2006-12-08
* Subtac bug fix, add list take example.Gravatar msozeau2006-12-08
* MAJGravatar herbelin2006-12-03
* Remplacement de la dépendance de G_vernac en G_constr (sourceGravatar herbelin2006-12-03
* add a comment about Show Existentials and a question about case_eq Gravatar jnarboux2006-12-01
* Fork of cases impl for subtac.Gravatar msozeau2006-11-29
* correction du bug : VM value extraction error (PR#1290)Gravatar bgregoir2006-11-29
* The $(BEST) binaries symlinks depend on existence of target, not newness.Gravatar lmamane2006-11-27
* Functional graph merging deals with letins.Gravatar courtieu2006-11-24
* Fixed the graph merging parameter order.Gravatar courtieu2006-11-24
* Fixed the -emacs option which was always On.Gravatar courtieu2006-11-24
* Fixing syntax and parameter order in functional graph merging.Gravatar courtieu2006-11-23
* Code mort découvert par MatthieuGravatar herbelin2006-11-22
* Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deGravatar herbelin2006-11-21
* un caractere blanc parasite dans svn:ignoreGravatar letouzey2006-11-21
* Changing merging functional scheme syntax.Gravatar courtieu2006-11-20
* Correction boucle du parseur en cas de caractÃère non unicodeGravatar herbelin2006-11-20
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* Dépendance inutile en Tacexpr, de proofs, qui se compile en principe aprèsGravatar herbelin2006-11-19
* mult_sym, plus_sym -> mult_comm, plus_commGravatar herbelin2006-11-19
* MAJGravatar herbelin2006-11-19
* Raffinement de l'unification de "apply": mémorisation de certainsGravatar herbelin2006-11-19
* Code mort (duplication de code dans reductionops.ml)Gravatar herbelin2006-11-18
* The emacs-U option now does not output *any* char above 250.Gravatar courtieu2006-11-17
* Small fix in functional graph merging.Gravatar courtieu2006-11-16
* suppression de code mort (avec bug de nom)Gravatar letouzey2006-11-16
* pb avec r9379 + modifs dans ringGravatar barras2006-11-16
* Work on dep types pattern matchingGravatar msozeau2006-11-16
* suite de r9362: reconnaissance de qqs injections entre nat, N et ZGravatar barras2006-11-16
* Adaptation à FreeBSDGravatar notin2006-11-16
* Some usability enhancements.Gravatar msozeau2006-11-15
* Better solve using tactics impl.Gravatar msozeau2006-11-13
* Correction de la seconde partie du bug #1278Gravatar jforest2006-11-13
* Correction de la premiere partie du #1278 (but non referme en cas d'echec)Gravatar jforest2006-11-13