aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-02-04Ajout constructeur External pour appel outil externe à Coqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6680 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Parseur pour la DTD XML de constr et un peu plus pour les arguments de tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6679 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Ajout constructeur External pour appel outil externe à Coqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6678 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Ajout d'un processus de communication entre Coq et un outil externeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6677 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Suppression de l'Unboxed des opérations sur positive (cf bug 898)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6676 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Essai d'utilisation de 'where' pour les notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6675 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6673 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Clarification des niveaux pr_constr et pr_lconstr en v8 dans pr_prim_rule ↵herbelin
(cut, refine, etc était en lconstr par erreur) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6672 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Tactics.v bidon pour accomoder make world7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6671 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6670 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03legere simplification des preuves de le_S_n et pred_leletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6669 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Implemented a test for "Add [Semi] Setoid Ring" to check that the givensacerdot
compatibility proofs are the default compatibility proofs for their respective operation. This closes a bug reported by Pierre Letouzey on coqdev. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6668 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Trivial bug fixed in "Add [Semi] Setoid Ring". An "&" in place of an "||"sacerdot
prevendent detection of only one mistake in the user input. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6667 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6666 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-02test de la bonne position des vars de ltac entre les vars et les relsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6664 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6663 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-02The statement of the compatibility theorem for addition and multiplicationsacerdot
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
2005-02-02 setoid_rewrite t; [tac]sacerdot
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
2005-02-02Correction de la précédence des contexts de variables rel, ltac et varherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6660 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6657 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-01Application du patch ebuild coq-8.0-r1 de la gentoo (uniformisation du Makefile)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6656 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-31majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6653 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-31Petit changement dans la gestion des nouveaux labels d'état (pour lecoq
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
2005-01-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6650 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6648 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6646 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6644 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6642 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-26Ajout cas VernacBackToherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6641 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-25Ajout dependance LIBCOQRUN pour coqide et coq-interfaceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6638 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-25sed ne connait pas '+' sur macosxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6636 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6634 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6632 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6629 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6625 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas ↵herbelin
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
2005-01-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6623 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Pour cible make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6620 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6610 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6608 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6606 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-18Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of thesacerdot
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
2005-01-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6603 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6602 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-17Bug fixed (reported by Roland): the setoire_rewrite in tactic did not worksacerdot
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
2005-01-171. added code to handle the inclusion of inductive types and constructors insacerdot
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
2005-01-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6598 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 20:39:52 +0000