From 8ad2627de29639b21473783195905dca6bb1c6ae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 Apr 2016 18:33:28 +0200
Subject: Getting rid of the Geninterp.generic_interp function.

---
 engine/geninterp.ml  | 5 -----
 engine/geninterp.mli | 2 --
 2 files changed, 7 deletions(-)

(limited to 'engine')

diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index 0d67213674..be4011cb64 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -28,8 +28,3 @@ module Interp = Register(InterpObj)
 
 let interp = Interp.obj
 let register_interp0 = Interp.register0
-
-let generic_interp ist (GenArg (Glbwit wit, v)) =
-  let open Ftactic.Notations in
-  interp wit ist v >>= fun ans ->
-  Ftactic.return (Val.inject (val_tag (topwit wit)) ans)
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 0992db7a29..0e7ed18471 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -21,7 +21,5 @@ 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, Val.t) interp_fun
-
 val register_interp0 :
   ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit
-- 
cgit v1.2.3