aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
2005-02-02test de la bonne position des vars de ltac entre les vars et les relsherbelin
2005-02-02majcoq
2005-02-02The statement of the compatibility theorem for addition and multiplicationsacerdot
2005-02-02 setoid_rewrite t; [tac]sacerdot
2005-02-02Correction de la précédence des contexts de variables rel, ltac et varherbelin
2005-02-01majcoq
2005-02-01Application du patch ebuild coq-8.0-r1 de la gentoo (uniformisation du Makefile)herbelin
2005-01-31majcoq
2005-01-31Petit changement dans la gestion des nouveaux labels d'état (pour lecoq
2005-01-30majcoq
2005-01-29majcoq
2005-01-28majcoq
2005-01-27majcoq
2005-01-26majcoq
2005-01-26Ajout cas VernacBackToherbelin
2005-01-25majcoq
2005-01-25Ajout dependance LIBCOQRUN pour coqide et coq-interfaceherbelin
2005-01-25sed ne connait pas '+' sur macosxherbelin
2005-01-24majcoq
2005-01-23majcoq
2005-01-22majcoq
2005-01-21majcoq
2005-01-21Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas toujour...herbelin
2005-01-21MAJherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-21Pour cible make docherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 04:48:13 +0000