diff options
Diffstat (limited to 'tactics/geninterp.mli')
| -rw-r--r-- | tactics/geninterp.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli index 472ff10901..34261c507c 100644 --- a/tactics/geninterp.mli +++ b/tactics/geninterp.mli @@ -17,8 +17,7 @@ type interp_sign = { lfun : Val.t Id.Map.t; extra : TacStore.t } -type ('glb, 'top) interp_fun = interp_sign -> - Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top +type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun |