diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e9102e9c82..8bf6e48fdb 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -333,15 +333,17 @@ let discharge_Function (_,finfos) = } let pr_ocst c = - Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) + let sigma, env = Pfedit.get_current_context () in + Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) let pr_info f_info = + let sigma, env = Pfedit.get_current_context () in str "function_constant := " ++ - Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ + Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ (try - Printer.pr_lconstr - (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant))) + Printer.pr_lconstr_env env sigma + (fst (Global.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 () ++ @@ -349,7 +351,7 @@ let pr_info f_info = str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ - str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () + str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in @@ -550,11 +552,11 @@ type tcc_lemma_value = | Value of constr | Not_needed -(* We only "purify" on exceptions *) +(* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try f x with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e |