diff options
author | 2008-04-23 21:29:34 +0000 | |
---|---|---|
committer | 2008-04-23 21:29:34 +0000 | |
commit | 37c82d53d56816c1f01062abd20c93e6a22ee924 (patch) | |
tree | ea8dcc10d650fe9d3b0d2e6378119207b8575017 /pretyping/evd.mli | |
parent | 3cea553e33fd93a561d21180ff47388ed031318e (diff) |
Prise en compte des coercions dans les clauses "with" même si le type
de l'argument donné contient des métavariables (souhait
#1408). Beaucoup d'infrastructure autour des constantes pour cela mais
qu'on devrait pouvoir récupérer pour analyser plus finement le
comportement des constantes en général :
1- Pour insérer les coercions, on utilise une transformation
(expérimentale) de Metas vers Evars le temps d'appeler coercion.ml.
2- Pour la compatibilité, on s'interdit d'insérer une coercion entre
classes flexibles parce que sinon l'insertion de coercion peut prendre
précédence sur la résolution des evars ce qui peut changer les
comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN).
3- Pour se souvenir rapidement de la nature flexible ou rigide du
symbole de tête d'une constante vis à vis de l'évaluation, on met en
place une table associant à chaque constante sa constante de tête (heads.ml)
4- Comme la table des constantes de tête a besoin de connaître
l'opacité des variables de section, la partie tables de declare.ml va
dans un nouveau decls.ml.
Au passage, simplification de coercion.ml, correction de petits bugs
(l'interface de Gset.fold n'était pas assez générale; specialize
cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml];
whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml])
et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml,
classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r-- | pretyping/evd.mli | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 352d3021d..71c6bb0dc 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -122,11 +122,28 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted type instance_constraint = IsSuperType | IsSubType | ConvUpToEta of int | UserGiven +(* Status of the unification of the type of an instance against the type of + the meta it instantiates: + - CoerceToType means that the unification of types has not been done + and that a coercion can still be inserted: the meta should not be + substituted freely (this happens for instance given via the + "with" binding clause). + - TypeProcessed means that the information obtainable from the + unification of types has been extracted. + - TypeNotProcessed means that the unification of types has not been + done but it is known that no coercion may be inserted: the meta + can be substituted freely. +*) + type instance_typing_status = CoerceToType | TypeNotProcessed | TypeProcessed +(* Status of an instance together with the status of its type unification *) + type instance_status = instance_constraint * instance_typing_status +(* Clausal environments *) + type clbinding = | Cltyp of name * constr freelisted | Clval of name * (constr freelisted * instance_status) * constr freelisted @@ -198,6 +215,7 @@ val meta_merge : evar_defs -> evar_defs -> evar_defs val undefined_metas : evar_defs -> metavariable list val metas_of : evar_defs -> metamap +val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs type metabinding = metavariable * constr * instance_status |