| Age | Commit message (Expand) | Author |
|---|
| 2005-01-15 | maj | coq |
| 2005-01-14 | maj | coq |
| 2005-01-14 | maj | coq |
| 2005-01-14 | Ajout de la syntaxe du reset label: "BackTo n". | coq |
| 2005-01-14 | Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed | sacerdot |
| 2005-01-14 | Affichage numéro de l'état de la commande courante pour mode emacs | herbelin |
| 2005-01-14 | Ajout mémorisation numéro commande courante + reset vers ce numéro pour mo... | herbelin |
| 2005-01-14 | Code redondant (cf Printer) | herbelin |
| 2005-01-13 | maj | coq |
| 2005-01-13 | Amélioration message Locate | herbelin |
| 2005-01-13 | Construct "T with (Definition|Module) id := c" generalized to | sacerdot |
| 2005-01-12 | maj | coq |
| 2005-01-12 | This commit corrects the last commit of Hugo that broke down the "make depend" | sacerdot |
| 2005-01-12 | The new tutorial on (co)inductive types by Pierre Casteran. | sacerdot |
| 2005-01-11 | maj | coq |
| 2005-01-10 | maj | coq |
| 2005-01-09 | maj | coq |
| 2005-01-08 | maj | coq |
| 2005-01-07 | maj | coq |
| 2005-01-06 | maj | coq |
| 2005-01-06 | - Module/Declare Module syntax made more uniform: | sacerdot |
| 2005-01-05 | maj | coq |
| 2005-01-05 | [ Waiting for a keyword to control expansion during functor application ] | sacerdot |
| 2005-01-04 | maj | coq |
| 2005-01-03 | maj | coq |
| 2005-01-03 | maj | coq |
| 2005-01-03 | HUGE COMMIT | sacerdot |
| 2005-01-03 | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin |
| 2005-01-02 | maj | coq |
| 2005-01-02 | maj | coq |
| 2005-01-02 | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin |
| 2005-01-02 | Réactivation d'un outil d'affichage pour le débogueur compatible avec ocaml... | herbelin |
| 2005-01-02 | Pour permettre le chargement des printers en ocamldebug >= 3.07 : renommage s... | herbelin |
| 2005-01-02 | MAJ | herbelin |
| 2005-01-02 | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin |
| 2005-01-02 | Découpage des printers pour ne pas avoir de dépendances en la vm dans les p... | herbelin |
| 2005-01-02 | Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan... | herbelin |
| 2005-01-01 | maj | coq |
| 2005-01-01 | Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac... | herbelin |
| 2004-12-31 | maj | coq |
| 2004-12-31 | Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac... | herbelin |
| 2004-12-31 | Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr... | herbelin |
| 2004-12-31 | Compatibilité ancien nom de ocamldebug-coq | herbelin |
| 2004-12-31 | Remplacement ocamldebug-v7 par lien symbolique ne marche pas, finalement, crÃ... | herbelin |
| 2004-12-31 | Remplacement ocamldebug-v7 par ocamldebug-coq (2ème) | herbelin |
| 2004-12-30 | maj | coq |
| 2004-12-30 | Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ... | herbelin |
| 2004-12-29 | maj | coq |
| 2004-12-29 | maj | coq |
| 2004-12-29 | ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien... | herbelin |
