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/funind/indfun_common.ml | |
| parent | 0c297ad43bd4b0b8187aa56756334bd294a212ca (diff) | |
| parent | b21cd4620e0983a23dd11c0f582bf367662aeee3 (diff) | |
Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 () ++ |