aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2006-01-04Restauration des commandes de débogage PrintConstr et PrintPureConstr ↵herbelin
(suite): correction des dépendances (et notamment non-dépendance en unix.cma) pour la création de printers.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7787 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7786 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04Remise en place des commandes vernaculaires PrintConstr et PrintPureConstr ↵herbelin
(débranchées depuis mars 01) + affichage plus concis des locations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7785 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04Achèvement du commit incomplet de la révision 1.110 (cvs log ↵herbelin
toplevel/metasyntax.ml) sur les formats de notations récursives + ajout de cassure par défaut en cas de notation récursive sans séparateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7783 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7781 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-03Modification pour que l'ordre des éléments respecte l'ordre dans lequel ↵herbelin
ils ont été déclarés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7780 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-03Redéclaration de la notation à l'import pour être cohérent avec ↵herbelin
l'activation à l'import des notations qui ne sont pas des définitions syntaxiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7779 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7775 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-02Affichage de 'O' (lettre) comme '0' (chiffre)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7774 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7772 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-31majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7770 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7768 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Application du souhait de transparence de well_founded_ltof (#1007)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7766 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Test bug #1025herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7765 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Correction dépendance g_prim.ml4/q_coqast.ml4herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7763 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵herbelin
de chaîne de caractères tel que "foo" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Mini-restructurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7761 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Nettoyage coqlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7760 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Nettoyage coqlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7759 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Ajout booléens; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7758 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7756 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-29La distribution de Rocq/GRAPHS se fait via le serveur de contributions ↵herbelin
utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7755 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7753 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 22:11:22 +0000