Finalement VTactic est gardé pour y plonger les tactiques ML, le

VTactic utilisé pour les fermetures de ltac s'appelle maintenant VTacticClos


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2693 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 11 insertions, 21 deletions

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 8955babfd..e3d2a3670 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -41,9 +41,10 @@ let err_msg_tactic_not_found macro_loc macro =
 
 (* Values for interpretation *)
 type value =
-  | VTactic of interp_sign * Coqast.t
+  | VTacticClos of interp_sign * Coqast.t
   | VFTactic of tactic_arg list * string
   | VRTactic of (goal list sigma * validation)
+  | VTactic of tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *)
   | VContext of interp_sign * Coqast.t * Coqast.t list
   | VArg of tactic_arg
   | VFun of (identifier * value) list * identifier option list * Coqast.t
@@ -489,7 +490,7 @@ let rec val_interp ist ast =
           | Some g -> match_context_interp ist ast lmr g)
     | Node(_,"MATCH",lmr) -> match_interp ist ast lmr
     (* Delayed evaluation *)
-    | Node(loc,("LETCUT"|"IDTAC"|"FAIL"|"PROGRESS"|"TACTICLIST"|"DO"|"TRY"|"INFO"|"REPEAT"|"ORELSE"|"FIRST"|"TCLSOLVE"),_) -> VTactic (ist,ast)
+    | Node(loc,("LETCUT"|"IDTAC"|"FAIL"|"PROGRESS"|"TACTICLIST"|"DO"|"TRY"|"INFO"|"REPEAT"|"ORELSE"|"FIRST"|"TCLSOLVE"),_) -> VTacticClos (ist,ast)
     (* Arguments and primitive tactics *)
     | Node(_,"VOID",[]) -> VVoid
     | Nvar(_,s) ->
@@ -555,7 +556,7 @@ let rec val_interp ist ast =
           (str "Unrecognizable ast: " ++ print_ast ast)) in
   if ist.debug = DebugOn then
     match debug_prompt ist.goalopt ast with
-    | Exit -> VTactic (ist,Node(dummy_loc,"IDTAC",[]))
+    | Exit -> VTacticClos (ist,Node(dummy_loc,"IDTAC",[]))
     | v -> value_interp {ist with debug=v}
   else
     value_interp ist
@@ -606,17 +607,19 @@ and app_interp ist fv largs ast =
 (* Gives the tactic corresponding to the tactic value *)
 and tactic_of_value vle g =
   match vle with
-  | VTactic (ist,tac) -> eval_tactic ist tac g
+  | VTacticClos (ist,tac) -> eval_tactic ist tac g
   | VFTactic (largs,f) -> (interp_atomic f largs g) 
   | VRTactic res -> res
+  | VTactic tac -> tac g
   | _ -> raise NotTactic
 
 (* Evaluation with FailError catching *)
 and eval_with_fail interp ast goal =
   try 
     (match interp ast with
-    | VTactic (ist,tac) -> VRTactic (eval_tactic ist tac goal)
+    | VTacticClos (ist,tac) -> VRTactic (eval_tactic ist tac goal)
     | VFTactic (largs,f) -> VRTactic (interp_atomic f largs goal)
+    | VTactic tac -> VRTactic (tac goal)
     | a -> a)
   with | FailError lvl ->
     if lvl = 0 then
@@ -971,7 +974,7 @@ and tac_interp lfun lmatch debug ast g =
     "Interpretation gives a non-tactic value") *)
 
 (*    match (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) with
-      | VTactic tac -> (tac g)
+      | VTacticClos tac -> (tac g)
       | VFTactic (largs,f) -> (f largs g) 
       | VRTactic res -> res
       | _ ->
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 188811c64..6dfcb73d8 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -20,9 +20,10 @@ open Term
 
 (* Values for interpretation *)
 type value =
-  | VTactic of interp_sign * Coqast.t
+  | VTacticClos of interp_sign * Coqast.t
   | VFTactic of tactic_arg list * string
   | VRTactic of (goal list sigma * validation)
+  | VTactic of tactic
   | VContext of interp_sign * Coqast.t * Coqast.t list
   | VArg of tactic_arg
   | VFun of (identifier * value) list * identifier option list * Coqast.t
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 56f760723..7f29b4358 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -109,7 +109,6 @@ let rec tauto_intuit t_reduce t_solver ist =
       $t_solver
    ) >>
 
-(*
 let unfold_not_iff = function
   | None -> interp <:tactic<Unfold not iff>>
   | Some id ->
@@ -119,19 +118,6 @@ let unfold_not_iff = function
 let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
 
 let t_reduction_not_iff = valueIn (VTactic reduction_not_iff)
-*)
-
-let reduction_not_iff ist =
-  match ist.goalopt with 
-    | None -> anomaly "reduction_not_iff"
-    | Some gl ->
-	List.fold_right
-	(fun id tac -> 
-	  let id = nvar id in <:tactic<Unfold not iff in $id; $tac>>)
-	(Tacmach.pf_ids_of_hyps gl)
-	<:tactic<Unfold not iff>>
-
-let t_reduction_not_iff = tacticIn reduction_not_iff
 
 let intuition_gen tac =
   interp (tacticIn (tauto_intuit t_reduction_not_iff tac))