diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/table.ml | 7 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 |
2 files changed, 5 insertions, 4 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 diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6fe6888f3d..61fbca23f2 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -342,7 +342,7 @@ let pr_info f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr - (Global.type_of_global_unsafe (ConstRef f_info.function_constant)) + (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ |