aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-02-05Localisation des libraries compilées uniquement via la structure du ↵herbelin
loadpath (sinon des modules de même nom chargés via un Export sont trouvés avant ceux officiellement dans le chemin) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6689 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6687 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6686 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Bug synchronisation fonction connectherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6685 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Ajout g_xml.ml4 et cic2Xml.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6684 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Ajout g_xml.ml4 et cic2Xml.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6683 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Ajout printer direct cic vers xmlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6682 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Export du printer xml vers tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6681 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@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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 23:02:15 +0000