diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-10-28 14:08:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:54 +0200 |
| commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
| tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /toplevel/search.ml | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'toplevel/search.ml')
| -rw-r--r-- | toplevel/search.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml index 1535ae617..37403504d 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -60,14 +60,15 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = with Not_found -> (* we are in a section *) () end | "CONSTANT" -> let cst = Global.constant_of_delta_kn kn in - let typ, _ = Environ.constant_type_in_ctx env cst in - fn (ConstRef cst) env typ + let gr = ConstRef cst in + let typ = Global.type_of_global_unsafe gr in + fn gr env typ | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in let iter_packet i mip = let ind = (mind, i) in - let i = (ind, Univ.UContext.instance mib.mind_universes) in + let i = (ind, Inductive.inductive_instance mib) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in let len = Array.length mip.mind_user_lc in |