aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2003-12-23Renommages des hypotheses transformees car en raison des possibles ↵herbelin
dependances, il n'y a pas de garantie de pouvoir les effacer pour garder le meme nom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5131 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-09cc updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5082 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-02error messages adjustementcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5057 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-01Nouvelle tactique EExistsclrenard
Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Obsolete, cf Funind.v dans test-suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5037 85f007b7-540e-0410-9357-904b9bb8a0f7
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@5036 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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-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-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-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-25CC: added injection theorycorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 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-20Code simplification in CCcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4955 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Prise en compte renommagesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4950 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18correction suite ajout nouvelles tactiquesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4945 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4919 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Ordre standard pour l'associativiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4908 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Correction chemin de Zherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4904 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵barras
Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13factorisation et generalisation des clausesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Bug TacIdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4884 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Restructuration ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Noms/énoncés plus canoniquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4875 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12petits changements de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12les modifs depuis la 7.4letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4858 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12TODOletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Extraction Module M devient simplement Extraction Mletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4856 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4852 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10le pb du <<.v vu comme module>> engendre maintenant une erreurletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4851 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10message informant de l'ecriture d'un fichier extraitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4850 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10révision du traitement des axiomes non réalisésletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4849 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10essai d'extraction sous un moduleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4847 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09factorisation de (recursive) libraryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4843 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4842 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Added Instantiate ... incorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres ↵herbelin
positifs et naturels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4810 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Renommage canonique d'un lemme redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4807 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Déport des lemmes de Omega de ZArith vers OmegaLemmasherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4803 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Renommage canonique d'un lemme redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4799 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Extension de zarithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4790 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Protection contre les buts sans inegaliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4767 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Ajout CPatNotation, PrintVisibilityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4766 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵herbelin
entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4751 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Redirected some of the verbose jprover output through the Pp module.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4746 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵herbelin
associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 23:37:05 +0000