diff options
| author | Hugo Herbelin | 2020-09-13 14:37:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-29 22:24:02 +0200 |
| commit | 5cac24428e448c12ab292265bb2ffd1146b38c25 (patch) | |
| tree | 43713dc6730d53db67fa2a910650154dee1b91a1 /plugins/funind/indfun_common.mli | |
| parent | bee9998b0cde3c86888fcad8c0dccbeebb351032 (diff) | |
Almost fully moving funind to new proof engine.
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 |