diff options
| author | herbelin | 2006-10-28 19:35:09 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-28 19:35:09 +0000 |
| commit | 359e4ffe307d7d8dd250735373fc6354a58ecff5 (patch) | |
| tree | 7204cb80cb272118a7ee60e9790d91d0efd11894 /parsing | |
| parent | 8bcd34ae13010797a974b0f3c16df6e23f2cb254 (diff) | |
Extension du polymorphisme de sorte au cas des définitions dans Type.
(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/search.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/search.ml b/parsing/search.ml index 580cb790c4..e225d59a48 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -57,12 +57,12 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = fn (VarRef idc) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> - let kn = locate_constant (qualid_of_sp sp) in - let {const_type=typ} = Global.lookup_constant kn in + let cst = locate_constant (qualid_of_sp sp) in + let typ = Typeops.type_of_constant env cst in if refopt = None || head_const typ = constr_of_global (out_some refopt) then - fn (ConstRef kn) env typ + fn (ConstRef cst) env typ | "INDUCTIVE" -> let kn = locate_mind (qualid_of_sp sp) in let mib = Global.lookup_mind kn in |