aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5026 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Notation locale pour Rpowerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5025 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Ajout lemmes, simplification preuve de SeqPropherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5024 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5023 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Renommages de variables dans RIneqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5021 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Utilisation nom dans message d'erreur implicite pas trouveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5020 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Utilisation du total_order non constructifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5019 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Report de lemmes de Znumtheory dans Zabs ou BinIntherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5018 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Renommages discrets dans RIneq et Znumtheoryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5017 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-28Protection contre les renommages; redondancesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5016 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-28commands renomme en queries, command goto a la place de forward to backwardt omarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5015 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-28Simplest Demo on modulescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5014 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5013 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5012 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Suite commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5011 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Retour des _eq en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5010 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Qualification des noms utilisateurs en cas de collision avec un nom nouveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5009 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Monstrueuse inefficacite due a l'innocence du redacteur de la ligne vis a ↵herbelin
vis de l'evaluation stricte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5008 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Hint Destruct mal affichebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5007 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5006 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Reparation bug compilmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5005 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5004 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5003 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Ajout ne_stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5002 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Traduction de @; simplification traduction des identherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5001 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Renommage de tactiques ltac coincidant avec certaines tactiques primitivesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5000 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Protection contre les notations videsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4999 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Remplacement de l'indicateur de date "@" par 'at'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4998 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Export string_index_fromherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4997 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ↵herbelin
Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4996 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26just forgot something in previous commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4995 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26removal of CC.v lemata in cc (deprecated)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4994 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4993 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25Garder 'destruct using' a l'affichage ?herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4992 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25modif lexer: ident peut commencer par _barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25Version preliminaire pour la V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4990 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments ↵herbelin
recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4989 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25Traduction Print Proofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4988 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25CC: added injection theorycorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25textesmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4986 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4985 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4984 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24aboutmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4983 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4982 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24tentative de completion ESC-/ a la emacsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4981 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵herbelin
passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24Renoncement de la compatibilite des noms qualifies au profit de la ↵herbelin
compatibilite des arguments implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4979 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4978 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:42:34 +0000