aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
2006-09-24Tentative d'amélioration du message d'erreur en cas de paramètre non laisséherbelin
implicite dans une clause "in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9174 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-24Correction bug dans détection clause "in" mal formée quand le "in" estherbelin
donné alors même qu'il n'est pas utile car ne lie aucun argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9173 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-23Correction bug #1179 (result of Notation.decompose_notation_key in wrong orderherbelin
leading to wrong/failing printing of notations such as "- 1" or "1 -"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9167 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-23- Correction filtrage des notations impliquant un "match" : la présenceherbelin
des localisations empêchait toute unification des pattern de filtrage de réussir. - Ajout au passage d'unification des pattern modulo alpha. - Exemples dans Notations.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9163 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-22Protection List.fold_left2 (cf bug #1224)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9162 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-20Declarative Proof Language: main commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Export de fonctions d'interprétation acceptant des evars non résoluesherbelin
en entrée et en sortie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9107 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de ↵herbelin
famille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9032 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-03Extension des motifs disjonctifs au cas de disjonction de motifs multiplesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23documentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8983 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Légère mise à jourherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8973 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Added {measure x f} as a valid recursion order.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8969 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Changement du type d'argument 'TacticArgType X' en un typeherbelin
'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de pouvoir typer correctement les wit_tactic (auparavant le typage des wit_tactic était trop libéral et permettait de casser la subject-reduction). Amélioration au passage de l'affichage de la tactique "replace by" (module Extratactics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Réinitialisation de token_number à chaque compilation d'un nouveau fichier ↵notin
(fixe le bug #914) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8924 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Correction trou de subject-reduction de create_arg dans genarg.mliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8917 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour ↵herbelin
permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29The "clean integration of subtac" patch.msozeau
Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive). The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed. The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at TYPES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-24Adaptation de Coqdoc au nouveau add_globnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8861 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Retour version 8852 de constrintern.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8855 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Erreur commit constrintern.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8854 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Changement de précédence de l'argument du by de assert; ↵herbelin
conséquences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Modification de add_glob (support des modules dans Coqdoc)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8852 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-19Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8831 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28 r8931@thot: notin | 2006-04-28 16:19:38 +0200notin
Correction d'un bug dans add_glob (list_chop), avec ajout des list_drop_prefix dans lib/util.ml et de drop_dirpath_prefix dans library/libnames.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8768 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Typo dans précédent commit (8755); protection renforcée dans analyse ↵herbelin
clause in du cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8757 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27- Distinction explicite des parties paramètres et arguments dans le typeherbelin
des inductifs de la clause "in" du filtrage. - Débogage et extension du parseur xml (g_xml.ml4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8755 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27préparation de add_glob en vue d'isolement de la partie module pourherbelin
l'option glob-dump git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8746 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26- Utilisation d'abbréviations pour les types intervenant dans RCasesherbelin
- Factorisation du procédé de transformation Cases -> RCases dans Detyping - Rebranchement de la traduction XML pour Cases (interrompue depuis suppression traducteur) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8741 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-24Timide tentative de clarification du statut de l'opérateur de filtrageherbelin
PCase dans le type pattern: le type pattern est utilisé essentiellement dans ltac, il est normalement obtenu sans typage, et ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à part car sans le type, il est impossible de savoir le nombre d'arguments du constructeur puisque par définition du "if", ceux-ci ne sont pas liants et ne laissent pas dans la syntaxe concrète (résolution au passage du bug #1070, dû à un filtrage incomplet dans le passage de pattern à rawconstr permettant l'affichage des pattern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-14Si un fixpoint a plusieurs arguments, mais un seul de type inductif, letouzey
ce patch dispense d'ecrire le { struct .. } En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind, l'index de l'argument inductif devient un int option au lieu d'un int. Les deux cas possibles: - Some n : les situations autorisées auparavant, a savoir {struct} explicite, ou bien un seul argument au total - None : le cas nouveau, qui redonne un entier lors du passage de rawconstr à constr si l'on trouve effectivement un unique argument ayant un type inductif, et une erreur sinon. Pour l'instant, on cherche l'inductif dans le type de manière syntaxique, mais il est jouable de rajouter un poil de reduction (au moins delta). Dans le détail, voici les coins que ce patch influence: - parsing/g_xml.ml4: continue pour l'instant a attendre un index explicite via un element xml "recIndex" - contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà un cas ctv_ID_OPT_NONE correspondant à l'absence de struct. Par contre, dans le détail, le code pour un CFix utilise l'index de recurrence pour recouper au besoin le type du fixpoint en deux. Est-ce que je me gourre en supposant que si l'on a besoin de couper ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de l'impression d'un constr, et donc que l'index aura été correctement résolu ? - contrib/subtac/subtac_command.ml: - contrib/funind/indfun.ml: dans les deux cas, j'ai fait le service minimum, le struct reste obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas dur à adapter pour ceux qui comprennent ces parties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8718 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-07- Documentation of the Program tactics.msozeau
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-31Amendement impression evar pour affichage des Meta par 'info'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8675 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default ↵msozeau
uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22- Correction bug calcul mind_consnrealargs, introduit à la révisionherbelin
7833, et que la révision 8644 n'avait pas corrigé dans le bon sens; renommage en mind_consnrealdecls pour éviter la confusion de sens avec mind_nrealargs - Correction de la description du type one_inductive_body - Ajout test avec let-in dans params et dans type constructeur (fichier Case12.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau
May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-04Correction message d'erreur ltac et adoption du modèle de message de Tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8125 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-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-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-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-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-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-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-16Version préliminaire d'inversion de la compilation du filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7881 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7879 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Résidus du traducteur v7 -> v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7842 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Résidus du traducteur v7 -> v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 14:55:47 +0000