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/recdef.mli | |
| parent | c7ac5dc8036623a02ab4ad6d11469e040e78c004 (diff) | |
| parent | 0437339ccac602d692b5b8c071b77ac756805520 (diff) | |
Merge PR#803: Clean ssr
Diffstat (limited to 'plugins/funind/recdef.mli')
| -rw-r--r-- | plugins/funind/recdef.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index e1a072799e..f3d5e73320 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -2,10 +2,10 @@ open API (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : - Proof_type.tactic -> + Tacmach.tactic -> bool -> Names.Id.t list option -> - Proof_type.tactic + Tacmach.tactic val recursive_definition : bool -> Names.Id.t -> |