takes better account of the new possibility to pass a parametric count argument

to both 'do' and 'fail'


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

3 files changed, 17 insertions, 33 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 18f2cc934..41ce1c4c1 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -81,6 +81,7 @@ and ct_COMMAND =
   | CT_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST
   | CT_hints_immediate of ct_FORMULA_NE_LIST * ct_ID_LIST
   | CT_hints_resolve of ct_FORMULA_NE_LIST * ct_ID_LIST
+  | CT_hyp_search_pattern of ct_FORMULA * ct_IN_OR_OUT_MODULES
   | CT_implicits of ct_ID * ct_ID_LIST_OPT
   | CT_import_id of ct_ID_NE_LIST
   | CT_ind_scheme of ct_SCHEME_SPEC_LIST
@@ -628,7 +629,7 @@ and ct_TACTIC_COM =
   | CT_destruct of ct_ID_OR_INT
   | CT_dhyp of ct_ID
   | CT_discriminate_eq of ct_ID_OR_INT_OPT
-  | CT_do of ct_INT * ct_TACTIC_COM
+  | CT_do of ct_ID_OR_INT * ct_TACTIC_COM
   | CT_eapply of ct_FORMULA * ct_SPEC_LIST
   | CT_eauto of ct_ID_OR_INT_OPT * ct_ID_OR_INT_OPT
   | CT_eauto_with of ct_ID_OR_INT_OPT * ct_ID_OR_INT_OPT * ct_ID_NE_LIST_OR_STAR
@@ -636,7 +637,7 @@ and ct_TACTIC_COM =
   | CT_elim_type of ct_FORMULA
   | CT_exact of ct_FORMULA
   | CT_exists of ct_SPEC_LIST
-  | CT_fail of ct_INT * ct_STRING_OPT
+  | CT_fail of ct_ID_OR_INT * ct_STRING_OPT
   | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list
   | CT_firstorder of ct_TACTIC_OPT
   | CT_firstorder_using of ct_TACTIC_OPT * ct_ID_NE_LIST
@@ -748,8 +749,6 @@ and ct_TYPED_FORMULA =
 and ct_UNFOLD =
     CT_coerce_ID_to_UNFOLD of ct_ID
   | CT_unfold_occ of ct_ID * ct_INT_NE_LIST
-and ct_UNFOLD_LIST =
-    CT_unfold_list of ct_UNFOLD list
 and ct_UNFOLD_NE_LIST =
     CT_unfold_ne_list of ct_UNFOLD * ct_UNFOLD list
 and ct_USING =
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 3801e1a04..8ff97b0c7 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -270,6 +270,10 @@ and fCOMMAND = function
    fFORMULA_NE_LIST x1;
    fID_LIST x2;
    fNODE "hints_resolve" 2
+| CT_hyp_search_pattern(x1, x2) ->
+   fFORMULA x1;
+   fIN_OR_OUT_MODULES x2;
+   fNODE "hyp_search_pattern" 2
 | CT_implicits(x1, x2) ->
    fID x1;
    fID_LIST_OPT x2;
@@ -1513,7 +1517,7 @@ and fTACTIC_COM = function
    fID_OR_INT_OPT x1;
    fNODE "discriminate_eq" 1
 | CT_do(x1, x2) ->
-   fINT x1;
+   fID_OR_INT x1;
    fTACTIC_COM x2;
    fNODE "do" 2
 | CT_eapply(x1, x2) ->
@@ -1544,7 +1548,7 @@ and fTACTIC_COM = function
    fSPEC_LIST x1;
    fNODE "exists" 1
 | CT_fail(x1, x2) ->
-   fINT x1;
+   fID_OR_INT x1;
    fSTRING_OPT x2;
    fNODE "fail" 2
 | CT_first(x,l) ->
@@ -1867,10 +1871,6 @@ and fUNFOLD = function
    fID x1;
    fINT_NE_LIST x2;
    fNODE "unfold_occ" 2
-and fUNFOLD_LIST = function
-| CT_unfold_list l ->
-   (List.iter fUNFOLD l);
-   fNODE "unfold_list" (List.length l)
 and fUNFOLD_NE_LIST = function
 | CT_unfold_ne_list(x,l) ->
    fUNFOLD x;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 014061f6e..33b3488db 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -583,6 +583,10 @@ let xlate_quantified_hypothesis_opt = function
   | Some (AnonHyp n) -> xlate_int_to_id_or_int_opt n
   | Some (NamedHyp id) -> xlate_id_to_id_or_int_opt id;;
 
+let xlate_id_or_int = function
+    ArgArg n -> CT_coerce_INT_to_ID_OR_INT(CT_int n)
+  | ArgVar(_, s) -> CT_coerce_ID_to_ID_OR_INT(xlate_ident s);;
+
 let xlate_explicit_binding (loc,h,c) = 
   CT_binding (xlate_quantified_hypothesis h, xlate_formula c)
 
@@ -680,24 +684,6 @@ let xlate_one_unfold_block = function
   | (n::nums, qid) ->
       CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_to_int_ne_list n nums);;
 
-let xlate_lettac_clauses = function
-    (opt_l, l') ->
-      let res = 
-	(List.map 
-	   (function
-		(id, []) -> 
-		  CT_coerce_ID_to_UNFOLD(xlate_ident_or_metaid id)
-	      | (id, n::nums) ->
-	      CT_unfold_occ(xlate_ident_or_metaid id, nums_to_int_ne_list n nums)) l') in
-	match opt_l with
-	    Some (n::nums) ->
-	      CT_unfold_list
-	      	((CT_unfold_occ
-		    (CT_ident "Goal", nums_to_int_ne_list n nums))::res)
-	  | Some [] ->
-	      CT_unfold_list((CT_coerce_ID_to_UNFOLD(CT_ident "Goal"))::res)
-	  | None -> CT_unfold_list res;;
-
 let xlate_intro_patt_opt = function
     None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
   | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
@@ -808,8 +794,7 @@ and xlate_tactic =
    | TacFirst(t1::l)-> CT_first(xlate_tactic t1, List.map xlate_tactic l)
    | TacSolve([]) -> assert false
    | TacSolve(t1::l)-> CT_tacsolve(xlate_tactic t1, List.map xlate_tactic l)
-   | TacDo(ArgArg n, t) -> CT_do(CT_int n, xlate_tactic t)
-   | TacDo(ArgVar _, t) -> xlate_error "Parametric tacticals 'do'"
+   | TacDo(count, t) -> CT_do(xlate_id_or_int count, xlate_tactic t)
    | TacTry t -> CT_try (xlate_tactic t)
    | TacRepeat t -> CT_repeat(xlate_tactic t)
    | TacAbstract(t,id_opt) -> 
@@ -876,9 +861,9 @@ and xlate_tactic =
 		   (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
        CT_rec_tactic_in(tl, xlate_tactic t)
    | TacAtom (_, t) -> xlate_tac t 
-   | TacFail (ArgArg n,"") -> CT_fail(CT_int n, ctf_STRING_OPT_NONE)
-   | TacFail (ArgArg n,s) -> CT_fail(CT_int n, ctf_STRING_OPT_SOME (CT_string s))
-   | TacFail (ArgVar _, _) -> xlate_error "Parametric tacticals 'fail'"
+   | TacFail (count, "") -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
+   | TacFail (count, s) -> CT_fail(xlate_id_or_int count,
+				   ctf_STRING_OPT_SOME (CT_string s))
    | TacId "" -> CT_idtac ctf_STRING_OPT_NONE
    | TacId s -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
    | TacInfo t -> CT_info(xlate_tactic t)