aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-01-14Code mort du traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7865 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7863 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-13Correction du bug #1055coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7862 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7857 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-12Changing well founded induction to fix on accessibility proof in orderbertot
to prepare the possibility to define function with more that one argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7856 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-12Compatibilité prtermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7855 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7852 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Test conflictuel - ajouté pour mémoireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7849 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Test or-patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7848 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Ajout test notation récursiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7847 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Suppression traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7846 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11remove warnings that were left in the directory contrib/interfacebertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7844 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11removes several warnings in contrib/interfacebertot
Modifies the behavior of Recursive definition to produce goals instead of established theorems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7843 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Résidus du traducteur v7 -> v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7842 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7841 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Suite réorganisation des fonctions d'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7840 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7839 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Résidus du traducteur v7 -> v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7836 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7835 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Suppression résidus code v7 et traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7834 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-10Ajout de la longueur de l'arité des constructeurs dans one_inductive_body ↵herbelin
et dans case_info pour permettre l'indépendance de detyping (entre autres) envers l'environnement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7833 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7831 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-10Détection var inutile par ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7830 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7827 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-09Suppression redondance coerce_to_id dans Pcoq et constrintern et ↵herbelin
déplacement dans Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7824 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Prise en compte, enfin, du contexte des types de retour de ACases et RCasesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7823 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Prise en compte de notations numérales définies au niveau utilisateur+ ↵herbelin
légère restructuration + correction nécessité redéclarer syntaxe '{ _ }' dans le cas nouvelle notation basée sur '{ _ }' en -nois + suite nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7822 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Prise en compte de notations numérales définies au niveau utilisateur + ↵herbelin
traitement dans alias de motifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7821 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Enregistrement dans glob.dump des utilisations de notations numériques (qui ↵herbelin
peuvent maintenant être définies au niveau utilisateur) + divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7820 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Automatisation de l'utilisation de token primitifs dans les motifs de ↵herbelin
filtrage + prise en compte de notations numérales définies au niveau utilisateur+ légère restructuration git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7819 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Automatisation de l'utilisation de token primitifs dans les motifs de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7818 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Ajout rawconstr_of_aconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7817 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Fonctions de conversion rawconstr <-> cases_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7816 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7814 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-07Réorganisation; suppression code mort; documentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7813 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7812 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7810 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-06Petite modification de la gestion du '.' (jmn)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7807 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7804 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-05*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7803 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-05Amelioration de l'elimination des preuves (bugs #1052 et #950-II) (jmn)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7799 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-05Test choix conflit afficheur de nombres selon la présence ou pas d'une coercionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7798 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-05*** empty log message ***coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7797 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-05Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ↵herbelin
suppression des coercions permet aussi d'afficher un nombre, on choisit l'affichage qui n'introduit pas de délimiteurs si possible (exemple: avec 'Zpos 2', si Zpos est une coercion, on peut effacer la coercion et afficher 2 dans le type positive, ou bien garder la coercion afficher 'Zpos 2' comme 2 dans Z; dans certains cas - cf 4CT - il n'y a pas d'afficheur qui gère la coercion et il faut la retirer avant d'appliquer l'afficheur de nombre le plus interne) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7796 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-05Adding a man page for doqdoc (JMN)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7794 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7792 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04Suppression des coercions non seulement avant l'affichage des notations mais ↵herbelin
aussi avant l'affichage des notations primitives git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7788 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 00:18:47 +0000