From 89abe2a141b3baa11bf0e8bcdecaf68220251c6e Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 2 Jul 2013 14:46:47 +0000
Subject: Removed the ad-hod handling of wit_tacticn.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16615 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacintern.ml | 14 +++++++-------
 tactics/tacinterp.ml | 18 +++++++++---------
 tactics/tacsubst.ml  | 13 ++++++-------
 3 files changed, 22 insertions(+), 23 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6f0d7525d1..6d50c02e24 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -795,13 +795,7 @@ and intern_genarg ist x =
   | OptArgType _ -> app_opt (intern_genarg ist) x
   | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x
   | ExtraArgType s ->
-      match tactic_genarg_level s with
-      | Some n ->
-          (* Special treatment of tactic arguments *)
-          in_gen (glbwit (wit_tactic n)) (intern_tactic_or_tacarg ist
-	    (out_gen (rawwit (wit_tactic n)) x))
-      | None ->
-          snd (Genintern.generic_intern ist x)
+      snd (Genintern.generic_intern ist x)
 
 (** Other entry points *)
 
@@ -954,6 +948,12 @@ let () =
   in
   Genintern.register_intern0 wit_intro_pattern intern_intro_pattern
 
+let () =
+  let intern ist tac = (ist, intern_tactic_or_tacarg ist tac) in
+  for i = 0 to 5 do
+    Genintern.register_intern0 (wit_tactic i) intern
+  done
+
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 58c64a8317..67fa0ed7b2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1451,15 +1451,6 @@ and interp_genarg ist gl x =
     | OptArgType _ -> app_opt (interp_genarg ist gl) x
     | PairArgType _ -> app_pair (interp_genarg ist gl) (interp_genarg ist gl) x
     | ExtraArgType s ->
-      match tactic_genarg_level s with
-      | Some n ->
-        let f = VFun(extract_trace ist,ist.lfun,[],
-          out_gen (glbwit (wit_tactic n)) x)
-        in
-        (* Special treatment of tactic arguments *)
-        in_gen (topwit (wit_tactic n)) 
-	  (TacArg(dloc,valueIn (of_tacvalue f)))
-      | None ->
         let (sigma,v) = Geninterp.generic_interp ist gl x in
 	evdref:=sigma;
 	v
@@ -2068,6 +2059,15 @@ let () =
   let interp ist gl pat = (gl.sigma, interp_intro_pattern ist gl pat) in
   Geninterp.register_interp0 wit_intro_pattern interp
 
+let () =
+  let interp ist gl tac =
+    let f = VFun (extract_trace ist, ist.lfun, [], tac) in
+    (gl.sigma, TacArg (dloc, valueIn (of_tacvalue f)))
+  in
+  for i = 0 to 5 do
+    Geninterp.register_interp0 (wit_tactic i) interp
+  done
+
 (***************************************************************************)
 (* Other entry points *)
 
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 2e84d44258..0068856162 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -322,16 +322,15 @@ and subst_genarg subst (x:glob_generic_argument) =
   | OptArgType _ -> app_opt (subst_genarg subst) x
   | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x
   | ExtraArgType s ->
-      match Extrawit.tactic_genarg_level s with
-      | Some n ->
-          (* Special treatment of tactic arguments *)
-          in_gen (glbwit (Extrawit.wit_tactic n))
-            (subst_tactic subst (out_gen (glbwit (Extrawit.wit_tactic n)) x))
-      | None ->
-          Genintern.generic_substitute subst x
+      Genintern.generic_substitute subst x
 
 (** Registering *)
 
 let () = Genintern.register_subst0 wit_intro_pattern (fun _ v -> v)
 
+let () =
+  for i = 0 to 5 do
+    Genintern.register_subst0 (Extrawit.wit_tactic i) subst_tactic
+  done
+
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic
-- 
cgit v1.2.3