diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 28a9542167..b68b34ca35 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -27,10 +27,6 @@ let array_get_start a = (Array.length a - 1) (fun i -> a.(i)) -let id_of_name = function - Name id -> id - | _ -> raise Not_found - let locate qid = Nametab.locate qid let locate_ind ref = @@ -105,15 +101,6 @@ let const_of_id id = CErrors.user_err ~hdr:"IndFun.const_of_id" (str "cannot find " ++ Id.print id) -let def_of_const t = - match Constr.kind t with - Const sp -> - (try (match Environ.constant_opt_value_in (Global.env()) sp with - | Some c -> c - | _ -> assert false) - with Not_found -> assert false) - |_ -> assert false - [@@@ocaml.warning "-3"] let coq_constant s = UnivGen.constr_of_monomorphic_global @@ @@ -160,17 +147,6 @@ let save with_clean id const (locality,_,kind) hook = CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id - - -let cook_proof _ = - let (id,(entry,_,strength)) = Pfedit.cook_proof () in - (id,(entry,strength)) - -let get_proof_clean do_reduce = - let result = cook_proof do_reduce in - Proof_global.discard_current (); - result - let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () |