aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2003-11-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4977 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4976 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-23MAJsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4975 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-23Prise en compte des definitions locales dans les (co-)points-fixesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4974 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22Compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4973 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22Traitement plus clair, notamment pour Locate, de quand quoter les ↵herbelin
composantes de notations + contournement du fait que Lexer arrive apres Symbol git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4972 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22Bug introduit avec le 'Simpl f'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4970 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4969 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Suppression des niveaux videsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4968 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21ajout Pnat et Pcompare_antisymherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4967 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Ajout 'Simpl f'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4966 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Simplification; ajout Zcompare_antisymherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4965 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21ajout Pnat (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4964 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21ajout Pnat (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4963 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase ↵herbelin
et Pcompare_antisym git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4962 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Ajout Print Implicitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4961 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Tri et typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4960 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-29 23:02:30 +0000