diff options
| author | Emilio Jesus Gallego Arias | 2019-07-17 15:32:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-31 11:13:04 +0200 |
| commit | ce22c1cb3bca8381d9b0ebfef2fbf27e92418b0c (patch) | |
| tree | ad8845c4bca61bf752c597574d6df5ab352fbd94 /plugins/funind | |
| parent | 105269d6799356eb52f289e191217b153c3bdade (diff) | |
[funind] Move common `make_eq` to funind_common.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/gen_principle.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 1 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 5 |
4 files changed, 5 insertions, 9 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index a6c5e63ecf..72975d6871 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -15,10 +15,6 @@ open Indfun_common module RelDecl = Context.Rel.Declaration -let make_eq () = - try EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) - with _ -> assert false - (* Move to common *) let observe strm = if do_observe () diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 2d8d10a1f2..5cc3c96983 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -429,6 +429,10 @@ let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_gl let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") +let make_eq () = + try EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) + with _ -> assert false + let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *) match r with GlobRef.ConstRef sp -> EvalConstRef sp diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index a95b1242ac..0b8cbf6dc5 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -41,6 +41,7 @@ val refl_equal : EConstr.constr Lazy.t val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr +val make_eq : unit -> EConstr.constr val save : Id.t diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 90631d8e55..1407585bff 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -30,11 +30,6 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl (* raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) *) -let make_eq () = - try - EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) - with _ -> assert false - (***********************************************) (* [revert_graph kn post_tac hid] transforme an hypothesis [hid] having type Ind(kn,num) t1 ... tn res |