diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-17 14:26:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-17 15:44:38 +0200 |
| commit | 90d64647d3fd5dbf5c337944dc0038f0b19b8a51 (patch) | |
| tree | b33528c72730ec541a75e3d0baaead6789f4dcb9 /plugins/funind | |
| parent | d412844753ef25f4431c209f47b97b9fa498297d (diff) | |
Removing dead code.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 17 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
2 files changed, 0 insertions, 19 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f4a062732..8c3033d0c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -17,19 +17,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 @@ -270,10 +257,6 @@ let change_property_sort toSort princ princName = ) princ_info.params - -let pp_dur time time' = - str (string_of_float (System.time_difference time time')) - let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (compute_elim_sig old_princ_type).nparams in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d8f006f51..961266c9c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -10,7 +10,6 @@ open Term open Vars open Namegen open Environ -open Declareops open Entries open Pp open Names @@ -125,7 +124,6 @@ let lt = function () -> (coq_base_constant "lt") let le = function () -> (coq_base_constant "le") let ex = function () -> (coq_base_constant "ex") let nat = function () -> (coq_base_constant "nat") -let coq_sig = function () -> (coq_base_constant "sig") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded" |