diff options
| author | Pierre-Marie Pédrot | 2020-09-30 14:05:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-30 14:05:08 +0200 |
| commit | 1c919ed6fa476f0f7a16d69e58989f3d75104910 (patch) | |
| tree | 3fd1b2452b9af72f0dc2cd1929683ec544372874 /plugins/funind/indfun_common.mli | |
| parent | c63f7c8407ae151e61e5490803bb19169ad37a5c (diff) | |
| parent | be3a5ac947cb57499b668a3745439b15ff8c48a8 (diff) | |
Merge PR #13021: Almost fully moving funind to new proof engine
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 396db55458..7b7044fdaf 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -90,7 +90,7 @@ exception Defining_principle of exn exception ToShow of exn val is_strict_tcc : unit -> bool -val h_intros : Names.Id.t list -> Tacmach.tactic +val h_intros : Names.Id.t list -> unit Proofview.tactic val h_id : Names.Id.t val hrec_id : Names.Id.t val acc_inv_id : EConstr.constr Util.delayed @@ -102,7 +102,7 @@ val well_founded : EConstr.constr Util.delayed val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_reference -val list_rewrite : bool -> (EConstr.constr * bool) list -> Tacmach.tactic +val list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic val decompose_lam_n : Evd.evar_map |