aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2006-01-25exporting the global reference to the inductive " \/ " in coqlib andbertot
eq_rawconstr in topconstr to prepare the introduction of the new version of functionnal induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7928 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7926 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-24Suppression de la dépendance en Map.fold de ocaml dont la sémantique aherbelin
changé entre les version 3.08.4 et 3.09.0 (influe notamment sur l'ordre d'application des Hints de auto) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7925 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7923 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-23Oubli lors suppression traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7922 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-23Répercussion mise à jour de Pierre Casteran vis à vis du changement de ↵herbelin
statut du paramètre de Acc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7921 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-23Precisionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7920 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7918 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-22Application de la suggestion de Nicolas Magaud (#1060)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7917 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7915 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Variable inutiliséeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7914 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind ↵herbelin
est incompatible avec la préservation du type de Acc_intro (par uniformité de notations, x est finalement préféré) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7912 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Messages de idtac et fail peuvent maintenant être des listes de string, int ↵herbelin
et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7911 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Ajout de la contrainte que l'assertion doit être complètement prouvée ↵herbelin
dans 'assert by' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7910 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Messages de idtac et fail peuvent maintenant être des listes de string, int ↵herbelin
et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7909 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et ↵herbelin
fail peuvent maintenant être des listes de string, int et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7908 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Déplacement de pr_arg et pr_opt de Ppconstr vers Utilherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7907 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Backtrack commit précédent (incompatible avec le choix de prendre Idtac ↵herbelin
comme défaut pour ne rien faire) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7906 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Accherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7905 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7903 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-20Ajout de la contrainte de résoudre l'assertion dans 'assert by'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7902 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 02:41:31 +0000