diff options
| author | Maxime Dénès | 2017-07-17 07:47:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-17 07:47:31 +0200 |
| commit | 3a5dd0df47b83a1a46061f2a14761d3d9ad79fcb (patch) | |
| tree | 843408d6fa6a37307c0441d7fa81b3df6ae277e2 /plugins/extraction/table.ml | |
| parent | 0c297ad43bd4b0b8187aa56756334bd294a212ca (diff) | |
| parent | b21cd4620e0983a23dd11c0f582bf367662aeee3 (diff) | |
Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2642aeefa4..dff3548fd8 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -445,9 +445,10 @@ let error_MPfile_as_mod mp b = "Please "^s2^"use (Recursive) Extraction Library instead.\n")) let argnames_of_global r = - let typ = Global.type_of_global_unsafe r in + let env = Global.env () in + let typ, _ = Global.type_of_global_in_context env r in let rels,_ = - decompose_prod (Reduction.whd_all (Global.env ()) typ) in + decompose_prod (Reduction.whd_all env typ) in List.rev_map fst rels let msg_of_implicit = function @@ -878,7 +879,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = Global.type_of_global_unsafe (ConstRef kn) in + let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin |