diff options
| author | Emilio Jesus Gallego Arias | 2019-07-19 03:41:07 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-07 19:44:29 +0200 |
| commit | e3e2bec0f31390fe797d65961a14f7cd78bc4109 (patch) | |
| tree | fe5fbc579fedf22298ed72222976c78993afed38 /plugins/funind/indfun_common.mli | |
| parent | 0d61500c7137f93942a63a356226276c26edfd99 (diff) | |
[funind] Port indfun to the new tactic engine.
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index fff4711044..0815ca882a 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -38,7 +38,6 @@ val chop_rprod_n : int -> Glob_term.glob_constr -> val eq : EConstr.constr Lazy.t 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 |