aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* The statement of the compatibility theorem for addition and multiplicationGravatar sacerdot2005-02-02
| | | | | | | | | | | have been changed to match the new statement used by Add Setoid. NOTE: this reveals a missing check in the code. Indeed, "Add Setoid Ring" does not check if the provided compatibility theorems have the expected type. To be done in a future commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6662 85f007b7-540e-0410-9357-904b9bb8a0f7
* setoid_rewrite t; [tac]Gravatar sacerdot2005-02-02
| | | | | | | | | | | now used in place of setoid_replace ... with ... ; try (exact t) ; tac The new stricter version closes a bug reported by Pierre Letouzey on coqdev. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6661 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de la précédence des contexts de variables rel, ltac et varGravatar herbelin2005-02-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6660 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application du patch ebuild coq-8.0-r1 de la gentoo (uniformisation du Makefile)Gravatar herbelin2005-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6656 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit changement dans la gestion des nouveaux labels d'état (pour leGravatar coq2005-01-31
| | | | | | | | | backtrack en mode emacs): quand on fait un reset, on fait revenir le label courant au bon numéro (sinon d'anciens numéros toujours utilisés dans le buffer emacs deviennent obsolètes). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6652 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6650 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6648 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6646 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6644 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout cas VernacBackToGravatar herbelin2005-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6641 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout dependance LIBCOQRUN pour coqide et coq-interfaceGravatar herbelin2005-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6638 85f007b7-540e-0410-9357-904b9bb8a0f7
* sed ne connait pas '+' sur macosxGravatar herbelin2005-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6636 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6634 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6632 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6629 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6625 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas ↵Gravatar herbelin2005-01-21
| | | | | | toujours (mais nécessite une archive intègre sans .mli non déclarés) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6624 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour cible make docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6610 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6608 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of theGravatar sacerdot2005-01-18
| | | | | | | | term to be replaced in the term that is the morphism was done too early (before computing the "morphism family" parameters). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6605 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6603 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug fixed (reported by Roland): the setoire_rewrite in tactic did not workGravatar sacerdot2005-01-17
| | | | | | | | | | | | | | | | | | | | | | | | | | in the followin case: H : t < c1 H0: c1 < c2 ============= t' setoid_rewrite H0 in H Explanation: the tactic made a cut with H0: c1 < c2 =============== t < c2 and then did setoid_rewrite <- H0 in H. If c2 occurs in t, then the tactic may fail (due to wrong variance). The simple fix consists in changing "t < c2" to "let H := c2 in t{H/c2} < c2" and then perform an intro before proceeding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6601 85f007b7-540e-0410-9357-904b9bb8a0f7
* 1. added code to handle the inclusion of inductive types and constructors inGravatar sacerdot2005-01-17
| | | | | | | | | | | | | | | parameters. 2. however, the code is still not working if the parameters are referenced later on in the module signature. To fix this the representation of terms must be changed to unify references to constants, inductive types and constructors. 3. thus the code above is prefixed by an error that suggest to the user how to avoid the problem right now. Note: the above code has not been commented out to keep it in synch with the other changes in the kernel. However, it is dead code for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6600 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6598 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6595 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6592 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la syntaxe du reset label: "BackTo n".Gravatar coq2005-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
| | | | | | | | | to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body) instead of looking it up in the environment. A version of the same functions with the old type is put in Inductiveops (outside the kernel). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage numéro de l'état de la commande courante pour mode emacsGravatar herbelin2005-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6588 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout mémorisation numéro commande courante + reset vers ce numéro pour ↵Gravatar herbelin2005-01-14
| | | | | | mode emacs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6587 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code redondant (cf Printer)Gravatar herbelin2005-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6586 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration message LocateGravatar herbelin2005-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
| | | | | | | "T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6580 85f007b7-540e-0410-9357-904b9bb8a0f7
* This commit corrects the last commit of Hugo that broke down the "make depend"Gravatar sacerdot2005-01-12
| | | | | | | command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6578 85f007b7-540e-0410-9357-904b9bb8a0f7
* The new tutorial on (co)inductive types by Pierre Casteran.Gravatar sacerdot2005-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6577 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6575 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6573 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 01:44:25 +0000