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.

---
 ltac/rewrite.ml   | 6 ++++--
 ltac/tacinterp.ml | 3 ++-
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'ltac')

diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 97b2393a8d..cd8ce7e87a 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -613,8 +613,10 @@ let solve_remaining_by env sigma holes by =
     (** Only solve independent holes *)
     let indep = List.map_filter map holes in
     let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
-    let solve_tac = Geninterp.generic_interp ist tac in
-    let solve_tac = Ftactic.run solve_tac (fun _ -> Proofview.tclUNIT ()) in
+    let solve_tac = match tac with
+    | Genarg.GenArg (Genarg.Glbwit tag, tac) ->
+      Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ())
+    in
     let solve_tac = Tacticals.New.tclCOMPLETE solve_tac in
     let solve sigma evk =
       let evi =
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 90784f5e84..b9d074a3dc 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1569,7 +1569,8 @@ and interp_genarg ist x : Val.t Ftactic.t =
       let q = Value.cast (topwit wit2) q in
       Ftactic.return (Value.of_pair (val_tag wit1) (val_tag wit2) (p, q))
     | ExtraArg s ->
-      Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x)
+      Geninterp.interp wit ist x >>= fun x ->
+      Ftactic.return (in_gen (Topwit wit) x)
 
 (** returns [true] for genargs which have the same meaning
     independently of goals. *)
-- 
cgit v1.2.3