diff options
| author | Matthieu Sozeau | 2013-10-28 14:08:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:54 +0200 |
| commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
| tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /plugins/extraction/table.ml | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 133f4ada9b..c48873c808 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -816,7 +816,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = (Environ.lookup_constant kn env).const_type in + let typ = Global.type_of_global_unsafe (ConstRef kn) in let typ = Reduction.whd_betadeltaiota env typ in if Reduction.is_arity env typ then begin |