aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-02-08Julien:bertot
+ Recursive definition (repository contrib/recdef) can now be used with GenFixpoint syntax by just replacing the usual {struct x} annotation by {wf R x} where x is one of the function declared arguments and R is a expression well-typed in the x typing environment. + Bug correction in new functional induction + For now no induction principle for general recursive definition is generated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8012 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Localisation des erreurs de sorte du prétypageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8011 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8010 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8009 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8007 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07oubli de code de debuggingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8006 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Messages nth brancheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8005 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Idem numbering of 'Unfold', 'simpl', ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8004 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Amélioration des messages d'erreurs de tacred; unfold considère maintenant leherbelin
prédicat de filtrage après le terme filtré conformément à l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8003 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Ajout pluralherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8002 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Mise en conformité de l'ordre des occurrences de pattern avec l'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8001 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8000 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7998 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et ↵herbelin
Russell O'Connor (redondance Acc_iter et Fix_F) + uniformisation indentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7997 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06warning seulement si mode verboseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7996 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06coq_makefileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7995 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06Ajout de l'essai d'effacement des noms des cibles custom par la cible cleanherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7994 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7992 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 19:26:28 +0000