| Commit message (Expand) | Author | Age |
* | Pas d'escamotage des noms réservés si Set Printing All actibvé | herbelin | 2006-12-08 |
* | Suite ajout option -output-context | herbelin | 2006-12-08 |
* | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 85f007b7-540e-04... | filliatr | 2006-12-08 |
* | Ajout d'une option -output-context qui affiche le contexte en CCI pur à la | herbelin | 2006-12-08 |
* | Correction typo règle réduction du fix chapitre CCI | herbelin | 2006-12-08 |
* | Subtac bug fix, add list take example. | msozeau | 2006-12-08 |
* | MAJ | herbelin | 2006-12-03 |
* | Remplacement de la dépendance de G_vernac en G_constr (source | herbelin | 2006-12-03 |
* | add a comment about Show Existentials and a question about case_eq | jnarboux | 2006-12-01 |
* | Fork of cases impl for subtac. | msozeau | 2006-11-29 |
* | correction du bug : VM value extraction error (PR#1290) | bgregoir | 2006-11-29 |
* | The $(BEST) binaries symlinks depend on existence of target, not newness. | lmamane | 2006-11-27 |
* | Functional graph merging deals with letins. | courtieu | 2006-11-24 |
* | Fixed the graph merging parameter order. | courtieu | 2006-11-24 |
* | Fixed the -emacs option which was always On. | courtieu | 2006-11-24 |
* | Fixing syntax and parameter order in functional graph merging. | courtieu | 2006-11-23 |
* | Code mort découvert par Matthieu | herbelin | 2006-11-22 |
* | Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de | herbelin | 2006-11-21 |
* | un caractere blanc parasite dans svn:ignore | letouzey | 2006-11-21 |
* | Changing merging functional scheme syntax. | courtieu | 2006-11-20 |
* | Correction boucle du parseur en cas de caractÃère non unicode | herbelin | 2006-11-20 |
* | Suppression du type 'tac dans les abstract_argument_type: devenu inutile | herbelin | 2006-11-20 |
* | Dépendance inutile en Tacexpr, de proofs, qui se compile en principe après | herbelin | 2006-11-19 |
* | mult_sym, plus_sym -> mult_comm, plus_comm | herbelin | 2006-11-19 |
* | MAJ | herbelin | 2006-11-19 |
* | Raffinement de l'unification de "apply": mémorisation de certains | herbelin | 2006-11-19 |
* | Code mort (duplication de code dans reductionops.ml) | herbelin | 2006-11-18 |
* | The emacs-U option now does not output *any* char above 250. | courtieu | 2006-11-17 |
* | Small fix in functional graph merging. | courtieu | 2006-11-16 |
* | suppression de code mort (avec bug de nom) | letouzey | 2006-11-16 |
* | pb avec r9379 + modifs dans ring | barras | 2006-11-16 |
* | Work on dep types pattern matching | msozeau | 2006-11-16 |
* | suite de r9362: reconnaissance de qqs injections entre nat, N et Z | barras | 2006-11-16 |
* | Adaptation à FreeBSD | notin | 2006-11-16 |
* | Some usability enhancements. | msozeau | 2006-11-15 |
* | Better solve using tactics impl. | msozeau | 2006-11-13 |
* | Correction de la seconde partie du bug #1278 | jforest | 2006-11-13 |
* | Correction de la premiere partie du #1278 (but non referme en cas d'echec) | jforest | 2006-11-13 |
* | Corrige un bug de calcul du temps effectif cquand la dernière décimale est 0 | herbelin | 2006-11-13 |
* | Encore des _sym au lieu de _comm | herbelin | 2006-11-13 |
* | Correction typo | herbelin | 2006-11-13 |
* | Fichiers obsolètes | herbelin | 2006-11-11 |
* | Typo + ajout Qcanon.v | herbelin | 2006-11-11 |
* | Ajout de dépliage de l'énoncé, si besoin est, dans apply in | herbelin | 2006-11-10 |
* | generalisation de ring pour faire Ring_nf | barras | 2006-11-10 |
* | Work on mutual defs, various bug fixes. | msozeau | 2006-11-10 |
* | Correction d'un bug refine | herbelin | 2006-11-10 |
* | Work on pattern inequalities for pattern matching branches. | msozeau | 2006-11-10 |
* | Support for mutual defs in obligation handling. | msozeau | 2006-11-09 |
* | Changement des modifeurs par défaut dans CoqIDE (problème de compatibilité... | notin | 2006-11-07 |