diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a14b47393..533fbfaaa 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -15,25 +15,6 @@ open Misctypes exception Toberemoved_with_rel of int*constr exception Toberemoved - -let pr_elim_scheme el = - let env = Global.env () in - let msg = str "params := " ++ Printer.pr_rel_context env el.params in - let env = Environ.push_rel_context el.params env in - let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in - let env = Environ.push_rel_context el.predicates env in - let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in - let env = Environ.push_rel_context el.branches env in - let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in - let env = Environ.push_rel_context el.args env in - msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl - - -let observe s = - if do_observe () - then Pp.msg_debug s - - let pr_elim_scheme el = let env = Global.env () in let msg = str "params := " ++ Printer.pr_rel_context env el.params in |