diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/geninterp.ml | 7 | ||||
| -rw-r--r-- | engine/geninterp.mli | 2 |
2 files changed, 3 insertions, 6 deletions
diff --git a/engine/geninterp.ml b/engine/geninterp.ml index a3e494f5c0..ffc22f2213 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -86,16 +86,13 @@ type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t module InterpObj = struct - type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun + type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun let name = "interp" let default _ = None end module Interp = Register(InterpObj) -let interp wit ist v = - let f = Interp.obj wit in - let tag = val_tag (Topwit wit) in - Ftactic.bind (f ist v) (fun v -> Ftactic.return (Val.inject tag v)) +let interp = Interp.obj let register_interp0 = Interp.register0 diff --git a/engine/geninterp.mli b/engine/geninterp.mli index c92181027e..5799862110 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -64,4 +64,4 @@ type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun val register_interp0 : - ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit + ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit |