aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
| | | | | | | 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
* Ajout paramétricité du nom de la base de hint dans auto et trivialGravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7836 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout paramétricité du nom de la base de hint dans auto et trivialGravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7835 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression résidus code v7 et traducteurGravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7834 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la longueur de l'arité des constructeurs dans one_inductive_body ↵Gravatar herbelin2006-01-10
| | | | | | 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
* majGravatar coq2006-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7831 85f007b7-540e-0410-9357-904b9bb8a0f7
* Détection var inutile par ocaml 3.09Gravatar herbelin2006-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7830 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7827 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression redondance coerce_to_id dans Pcoq et constrintern et ↵Gravatar herbelin2006-01-09
| | | | | | déplacement dans Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7824 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte, enfin, du contexte des types de retour de ACases et RCasesGravatar herbelin2006-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de notations numérales définies au niveau utilisateur+ ↵Gravatar herbelin2006-01-08
| | | | | | 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
* Prise en compte de notations numérales définies au niveau utilisateur + ↵Gravatar herbelin2006-01-08
| | | | | | traitement dans alias de motifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enregistrement dans glob.dump des utilisations de notations numériques (qui ↵Gravatar herbelin2006-01-08
| | | | | | 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
* Automatisation de l'utilisation de token primitifs dans les motifs de ↵Gravatar herbelin2006-01-08
| | | | | | 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
* Automatisation de l'utilisation de token primitifs dans les motifs de filtrageGravatar herbelin2006-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7818 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout rawconstr_of_aconstrGravatar herbelin2006-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fonctions de conversion rawconstr <-> cases_patternGravatar herbelin2006-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7816 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7814 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation; suppression code mort; documentationGravatar herbelin2006-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7813 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7812 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite modification de la gestion du '.' (jmn)Gravatar coq2006-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7807 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7804 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2006-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration de l'elimination des preuves (bugs #1052 et #950-II) (jmn)Gravatar coq2006-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test choix conflit afficheur de nombres selon la présence ou pas d'une coercionGravatar herbelin2006-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7798 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar coq2006-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ↵Gravatar herbelin2006-01-05
| | | | | | 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
* Adding a man page for doqdoc (JMN)Gravatar coq2006-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7794 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7792 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des coercions non seulement avant l'affichage des notations mais ↵Gravatar herbelin2006-01-04
| | | | | | 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
* Restauration des commandes de débogage PrintConstr et PrintPureConstr ↵Gravatar herbelin2006-01-04
| | | | | | (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
* Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)Gravatar herbelin2006-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remise en place des commandes vernaculaires PrintConstr et PrintPureConstr ↵Gravatar herbelin2006-01-04
| | | | | | (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
* Achèvement du commit incomplet de la révision 1.110 (cvs log ↵Gravatar herbelin2006-01-04
| | | | | | 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
* majGravatar coq2006-01-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification pour que l'ordre des éléments respecte l'ordre dans lequel ↵Gravatar herbelin2006-01-03
| | | | | | ils ont été déclarés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7780 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redéclaration de la notation à l'import pour être cohérent avec ↵Gravatar herbelin2006-01-03
| | | | | | 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
* majGravatar coq2006-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage de 'O' (lettre) comme '0' (chiffre)Gravatar herbelin2006-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7774 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2006-01-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7772 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7770 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7768 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application du souhait de transparence de well_founded_ltof (#1007)Gravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test bug #1025Gravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction dépendance g_prim.ml4/q_coqast.ml4Gravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7763 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵Gravatar herbelin2005-12-30
| | | | | | 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
* Mini-restructurationGravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage coqlibGravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7760 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-28 18:51:37 +0000