diff options
| author | Maxime Dénès | 2017-06-20 08:09:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-20 08:09:00 +0200 |
| commit | 25cd7acea0df79fcc07274e429c9839de1246611 (patch) | |
| tree | 1ee95df49ec9ea7152afed41df425ea4e4760736 /plugins/funind/indfun_common.mli | |
| parent | c7ac5dc8036623a02ab4ad6d11469e040e78c004 (diff) | |
| parent | 0437339ccac602d692b5b8c071b77ac756805520 (diff) | |
Merge PR#803: Clean ssr
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 6b40c91713..f7a9cedd73 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -105,7 +105,7 @@ exception ToShow of exn val is_strict_tcc : unit -> bool -val h_intros: Names.Id.t list -> Proof_type.tactic +val h_intros: Names.Id.t list -> Tacmach.tactic val h_id : Names.Id.t val hrec_id : Names.Id.t val acc_inv_id : EConstr.constr Util.delayed @@ -114,7 +114,7 @@ val well_founded_ltof : EConstr.constr Util.delayed val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference -val list_rewrite : bool -> (EConstr.constr*bool) list -> Proof_type.tactic +val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t |