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 -----
 1 file changed, 5 deletions(-)

(limited to 'engine/geninterp.ml')

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)
-- 
cgit v1.2.3