From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- contrib/interface/centaur.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'contrib/interface/centaur.ml4') diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 8fcdb5d9..730e055b 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -396,7 +396,7 @@ let inspect n = let (_, _, v) = get_variable (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> - let {const_type=typ} = Global.lookup_constant (constant_of_kn kn) in + let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_sp sp)) -- cgit v1.2.3