aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* The statement of the compatibility theorem for addition and multiplicationGravatar sacerdot2005-02-02
* setoid_rewrite t; [tac]Gravatar sacerdot2005-02-02
* Correction de la précédence des contexts de variables rel, ltac et varGravatar herbelin2005-02-02
* majGravatar coq2005-02-01
* Application du patch ebuild coq-8.0-r1 de la gentoo (uniformisation du Makefile)Gravatar herbelin2005-02-01
* majGravatar coq2005-01-31
* Petit changement dans la gestion des nouveaux labels d'état (pour leGravatar coq2005-01-31
* majGravatar coq2005-01-30
* majGravatar coq2005-01-29
* majGravatar coq2005-01-28
* majGravatar coq2005-01-27
* majGravatar coq2005-01-26
* Ajout cas VernacBackToGravatar herbelin2005-01-26
* majGravatar coq2005-01-25
* Ajout dependance LIBCOQRUN pour coqide et coq-interfaceGravatar herbelin2005-01-25
* sed ne connait pas '+' sur macosxGravatar herbelin2005-01-25
* majGravatar coq2005-01-24
* majGravatar coq2005-01-23
* majGravatar coq2005-01-22
* majGravatar coq2005-01-21
* Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas toujour...Gravatar herbelin2005-01-21
* MAJGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Pour cible make docGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* majGravatar coq2005-01-20
* majGravatar coq2005-01-19
* majGravatar coq2005-01-18
* Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of theGravatar sacerdot2005-01-18
* majGravatar coq2005-01-17
* majGravatar coq2005-01-17
* Bug fixed (reported by Roland): the setoire_rewrite in tactic did not workGravatar sacerdot2005-01-17
* 1. added code to handle the inclusion of inductive types and constructors inGravatar sacerdot2005-01-17
* majGravatar coq2005-01-16
* majGravatar coq2005-01-15
* majGravatar coq2005-01-14
* majGravatar coq2005-01-14
* Ajout de la syntaxe du reset label: "BackTo n".Gravatar coq2005-01-14
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Affichage numéro de l'état de la commande courante pour mode emacsGravatar herbelin2005-01-14
* Ajout mémorisation numéro commande courante + reset vers ce numéro pour mo...Gravatar herbelin2005-01-14
* Code redondant (cf Printer)Gravatar herbelin2005-01-14
* majGravatar coq2005-01-13
* Amélioration message LocateGravatar herbelin2005-01-13
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* majGravatar coq2005-01-12
* This commit corrects the last commit of Hugo that broke down the "make depend"Gravatar sacerdot2005-01-12
* The new tutorial on (co)inductive types by Pierre Casteran.Gravatar sacerdot2005-01-12
* majGravatar coq2005-01-11
* majGravatar coq2005-01-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 01:52:04 +0000