aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-02-05Debugging en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7991 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7989 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04Branchement sur nouvelle interface de declare_numeral_interpreterherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7988 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04Recherche des global_reference paresseusement pour pouvoir interpréterherbelin
les chaînes dans le module en cours de compilation (sachant que le nom de module est alors différent que lors d'un Require) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7987 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04parsing/g_ascii_syntax.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7986 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04Ajout nat_path et find_referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7985 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04Utilisation du section_path pour le parsing des notations primitives,herbelin
dans la mesure où le nom d'un module est différent selon qu'on est en cours de compilation (MPself) ou requis (MPfile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7984 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7983 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7981 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-03added mli 's for the nex functional induction (forgotten last time).coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7980 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-03+ Adding an error message when the function cannot be definedbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7979 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7977 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7975 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-01protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7974 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-01protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7973 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-01New version of functional induction / inversion. By Julien Forest,coq
Benjamin Gregoire, Gilles Barthe. For the moment, it is as followed: If one uses GenFixpoint instead of Fixpoint, then induction principles are generated on the fly (respecting the match structure written by the user, with wildcards etc). These principles can be used directly or by tactics "new functional induction" and "functional inversion". We will soon make "new functional induction" become "functional induction", before release of V8.1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7972 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-01Optimisation filtrage sans lieurs (utile pour Ltac)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7970 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-31majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7968 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-31Adaptation message d'erreur au cas des stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7967 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-31Ajout de fichiers d'interprétation de la syntaxe primitive pour string et charherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7966 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-31Ajout décidabilitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7965 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7963 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Suppression fonctions d'interprétation du vieux Caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7962 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Prise en compte coercions autour des sous-termes filtrés (si non dépendants)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7961 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Gestion des erreurs pour nombre incorrect d'argument des constructeurs (et deherbelin
l'inductif si clause "in I ...") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7960 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrerherbelin
- Prise en compte coercions autour des sous-termes filtrés (si non dépendants) - Test du bon nombre d'argument des constructeurs (et de l'inductif si clause "in I ...") maintenant fait aussi dans constrintern, pour assurer notamment que les constructeurs et inductifs dans pattern (obtenu de rawconstr) ont les bonnes arités - Renommage v7 -> v8 dans commentaires git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7959 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Fonctions retournant les arits des constructeurs et inductifs (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7958 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Déplacement du test du bon nombre d'argument des constructeurs (et deherbelin
l'inductif si clause "in I ...") dans Constrintern, pour assurer notamment que les constructeurs et inductifs dans pattern (obtenu de rawconstr) ont les bonnes arités git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7957 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas laherbelin
bonne arité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7956 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Fonctions retournant les arits des constructeurs et inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7955 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Nettoyage warning (dont flush et affichage seulement si mode verbose)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7954 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;herbelin
- Prise en compte coercions autour des sous-termes filtrés (si non dépendants) - Renommage v7 -> v8 dans commentaires git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7953 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Ajout ppenvherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7952 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Plutôt pas de contraction des match dans le déboggueurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7951 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7949 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-29Documentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7948 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-29Ajout printer Idset.therbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7947 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-29Bug 'match x in I' (potentiellement utilisable comme cast)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7946 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-29MAJ (synonymes de Lemma; auto using)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7945 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-29Ajout syntaxe concrète Proposition, synonyme de Lemmaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7944 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7942 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28- Ajout syntaxe concrète Property/Corollary, synonymes de Lemmaherbelin
- Ajout syntaxe concrète Example, synonyme de Definition - Réorganisation de la structure interne des types de déclarations (decl_kinds) - Notamment, ajout de noms pour les déclarations interne (Scheme, Fixpoint...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7940 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28- Ajout syntaxe concrète Property/Corollary, synonymes de Lemmaherbelin
- Ajout syntaxe concrète Example, synonyme de Definition - Réorganisation de la structure interne des types de déclarations (decl_kinds) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7939 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Correction bug Inspect introduit par le passage du discharge à une méthode ↵herbelin
associée aux objects git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7938 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Ajout option 'using lemmas' à auto/trivial/eautoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7937 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Suppression code pour hints nommés à la V7 (voire à la V6...)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7936 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7934 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7932 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7930 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 09:42:02 +0000