diff options
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 1b4c1248a5..0c8f40c5cf 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -18,8 +18,6 @@ val get_name : Id.t list -> ?default:string -> Name.t -> Name.t val array_get_start : 'a array -> 'a array -val id_of_name : Name.t -> Id.t - val locate_ind : Libnames.qualid -> inductive val locate_constant : Libnames.qualid -> Constant.t val locate_with_msg : @@ -38,7 +36,6 @@ val chop_rlambda_n : int -> Glob_term.glob_constr -> val chop_rprod_n : int -> Glob_term.glob_constr -> (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr -val def_of_const : Constr.t -> Constr.t val eq : EConstr.constr Lazy.t val refl_equal : EConstr.constr Lazy.t val const_of_id: Id.t -> GlobRef.t(* constantyes *) |