diff options
Diffstat (limited to 'tactics/geninterp.mli')
| -rw-r--r-- | tactics/geninterp.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli index 7f25a022c..0992db7a2 100644 --- a/tactics/geninterp.mli +++ b/tactics/geninterp.mli @@ -14,15 +14,14 @@ open Genarg module TacStore : Store.S type interp_sign = { - lfun : tlevel generic_argument Id.Map.t; + 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 -val generic_interp : (glob_generic_argument, typed_generic_argument) interp_fun +val generic_interp : (glob_generic_argument, Val.t) interp_fun val register_interp0 : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit |