diff options
| author | Pierre-Marie Pédrot | 2018-10-26 13:50:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-26 13:50:12 +0200 |
| commit | 27266c1f79e565a6a19da4c79fc1ce83f748e31c (patch) | |
| tree | 865bd07aa81debed13d6c5b5f4b5b2d8d26d7443 /plugins/funind | |
| parent | 69cbb9c09d5a440461b945c6690745b444649fda (diff) | |
| parent | 2e53939f4ce4bc06a5e7b621bc560d3ebeb59110 (diff) | |
Merge PR #8687: Mini reorganization type of global constr of global
Diffstat (limited to 'plugins/funind')
| -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 a385a61ae0..28a9542167 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -311,7 +311,7 @@ let pr_info f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr_env env sigma - (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) + (fst (Typeops.type_of_global_in_context 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 () ++ |