From 37c82d53d56816c1f01062abd20c93e6a22ee924 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 23 Apr 2008 21:29:34 +0000 Subject: 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 --- contrib/interface/centaur.ml4 | 2 +- contrib/interface/name_to_ast.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'contrib/interface') diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index b825262005..a4dc0eacd3 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -408,7 +408,7 @@ let inspect n = oname, Lib.Leaf lobj -> (match oname, object_tag lobj with (sp,_), "VARIABLE" -> - let (_, _, v) = get_variable (basename sp) in + let (_, _, v) = Global.lookup_named (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 172c7479c2..6b17e7396a 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -158,7 +158,7 @@ let constant_to_ast_list kn = make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l) let variable_to_ast_list sp = - let (id, c, v) = get_variable sp in + let (id, c, v) = Global.lookup_named sp in let l = implicits_of_global (VarRef sp) in (match c with None -> -- cgit v1.2.3