diff options
| author | herbelin | 2008-04-23 21:29:34 +0000 |
|---|---|---|
| committer | herbelin | 2008-04-23 21:29:34 +0000 |
| commit | 37c82d53d56816c1f01062abd20c93e6a22ee924 (patch) | |
| tree | ea8dcc10d650fe9d3b0d2e6378119207b8575017 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/prettyp.ml | 10 | ||||
| -rw-r--r-- | parsing/search.ml | 4 |
2 files changed, 7 insertions, 7 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 48fe40cab2..6ca3a5c1a1 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -360,12 +360,12 @@ let gallina_print_inductive sp = (print_inductive_implicit_args sp mipv ++ print_inductive_argument_scopes sp mipv) -let print_named_decl sp = - gallina_print_named_decl (get_variable sp) ++ fnl () +let print_named_decl id = + gallina_print_named_decl (Global.lookup_named id) ++ fnl () -let gallina_print_section_variable sp = - print_named_decl sp ++ - with_line_skip (print_name_infos (VarRef sp)) +let gallina_print_section_variable id = + print_named_decl id ++ + with_line_skip (print_name_infos (VarRef id)) let print_body = function | Some lc -> pr_lconstr (Declarations.force lc) diff --git a/parsing/search.ml b/parsing/search.ml index fd9eb12bbb..88b51907b0 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -50,11 +50,11 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = let crible_rec (sp,_) lobj = match object_tag lobj with | "VARIABLE" -> (try - let (idc,_,typ) = get_variable (basename sp) in + let (id,_,typ) = Global.lookup_named (basename sp) in if refopt = None || head_const typ = constr_of_global (Option.get refopt) then - fn (VarRef idc) env typ + fn (VarRef id) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> let cst = locate_constant (qualid_of_sp sp) in |