aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-01-20majcoq
2005-01-19majcoq
2005-01-18majcoq
2005-01-18Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of thesacerdot
2005-01-17majcoq
2005-01-17majcoq
2005-01-17Bug fixed (reported by Roland): the setoire_rewrite in tactic did not worksacerdot
2005-01-171. added code to handle the inclusion of inductive types and constructors insacerdot
2005-01-16majcoq
2005-01-15majcoq
2005-01-14majcoq
2005-01-14majcoq
2005-01-14Ajout de la syntaxe du reset label: "BackTo n".coq
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
2005-01-14Affichage numéro de l'état de la commande courante pour mode emacsherbelin
2005-01-14Ajout mémorisation numéro commande courante + reset vers ce numéro pour mo...herbelin
2005-01-14Code redondant (cf Printer)herbelin
2005-01-13majcoq
2005-01-13Amélioration message Locateherbelin
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
2005-01-12majcoq
2005-01-12This commit corrects the last commit of Hugo that broke down the "make depend"sacerdot
2005-01-12The new tutorial on (co)inductive types by Pierre Casteran.sacerdot
2005-01-11majcoq
2005-01-10majcoq
2005-01-09majcoq
2005-01-08majcoq
2005-01-07majcoq
2005-01-06majcoq
2005-01-06- Module/Declare Module syntax made more uniform:sacerdot
2005-01-05majcoq
2005-01-05[ Waiting for a keyword to control expansion during functor application ]sacerdot
2005-01-04majcoq
2005-01-03majcoq
2005-01-03majcoq
2005-01-03HUGE COMMITsacerdot
2005-01-03Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin
2005-01-02majcoq
2005-01-02majcoq
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin
2005-01-02Réactivation d'un outil d'affichage pour le débogueur compatible avec ocaml...herbelin
2005-01-02Pour permettre le chargement des printers en ocamldebug >= 3.07 : renommage s...herbelin
2005-01-02MAJherbelin
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin
2005-01-02Découpage des printers pour ne pas avoir de dépendances en la vm dans les p...herbelin
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...herbelin
2005-01-01majcoq
2005-01-01Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...herbelin
2004-12-31majcoq
2004-12-31Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 00:44:21 +0000