diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-20 17:24:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-04 13:47:12 +0200 |
| commit | 729d838838d8df06395726477817620e2ae998bc (patch) | |
| tree | 50986942f010f2a9281aa19dd715bd1f67dd921e /engine | |
| parent | 4740e82e4af6d38e9cc55dfe1a05db87f73bf1e6 (diff) | |
Interpretation function can return any untyped value.
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 a3e494f5c..ffc22f221 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 c92181027..579986211 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 |