Généralisation de with_occurrence (ex occurrence) et de red_expr pour permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern

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

4 files changed, 32 insertions, 22 deletions

diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index bc4699ea19..a181851680 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -211,6 +211,6 @@ let normalize_evaluables=
   onAllClauses
     (function 
 	 None->unfold_in_concl (Lazy.force defined_connectives)
-       | Some (id,_,_)-> 
+       | Some ((_,id),_)-> 
 	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   (id,[],Tacexpr.InHypTypeOnly))
+	   (([],id),Tacexpr.InHypTypeOnly))
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 85a60bd1c0..2e5616f0e1 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -105,7 +105,7 @@ let invfun (hypname:identifier) fname princ : tactic=
       let frealargs = (snd (array_chop (List.length princ_info.params) fargs))  
       in
       let pat_args = 
-	(List.map (fun e -> ([-1],e)) (Array.to_list frealargs)) @ [[],appf] 
+	(List.map (fun e -> ([Rawterm.ArgArg (-1)],e)) (Array.to_list frealargs)) @ [[],appf] 
       in
       tclTHENSEQ 
 	[
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index b9cd78e0b2..deb8426658 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -113,8 +113,16 @@ let nums_to_int_list_aux l = List.map (fun x -> CT_int x) l;;
 
 let nums_to_int_list l =  CT_int_list(nums_to_int_list_aux l);;
 
-let nums_to_int_ne_list n l =
-  CT_int_ne_list(CT_int n, nums_to_int_list_aux l);;
+let num_or_var_to_int = function
+  | ArgArg x -> CT_int x
+  | _ -> xlate_error "TODO: nums_to_int_list_aux ArgVar";;
+
+let nums_or_var_to_int_list_aux l = List.map num_or_var_to_int l;;
+
+let nums_or_var_to_int_list l = CT_int_list(nums_or_var_to_int_list_aux l);;
+
+let nums_or_var_to_int_ne_list n l =
+  CT_int_ne_list(num_or_var_to_int n, nums_or_var_to_int_list_aux l);;
 
 type iTARG =   Targ_command of ct_FORMULA
              | Targ_intropatt of ct_INTRO_PATT_LIST
@@ -474,18 +482,19 @@ let xlate_hyp = function
 
 let xlate_hyp_location =
  function
-  | AI (_,id), nums, InHypTypeOnly ->
-      CT_intype(xlate_ident id, nums_to_int_list nums)
-  | AI (_,id), nums, InHypValueOnly ->
-      CT_invalue(xlate_ident id, nums_to_int_list nums)
-  | AI (_,id), [], InHyp ->
+  | (nums, AI (_,id)), InHypTypeOnly ->
+      CT_intype(xlate_ident id, nums_or_var_to_int_list nums)
+  | (nums, AI (_,id)), InHypValueOnly ->
+      CT_invalue(xlate_ident id, nums_or_var_to_int_list nums)
+  | ([], AI (_,id)), InHyp ->
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_coerce_ID_to_UNFOLD (xlate_ident id))
-  | AI (_,id), a::l, InHyp ->
+  | (a::l, AI (_,id)), InHyp ->
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_unfold_occ (xlate_ident id, 
-			CT_int_ne_list(CT_int a, nums_to_int_list_aux l)))
-  | MetaId _, _,_ -> 
+			CT_int_ne_list(num_or_var_to_int a, 
+                                       nums_or_var_to_int_list_aux l)))
+  | (_, MetaId _),_ -> 
       xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
 
 let xlate_clause cls =
@@ -666,7 +675,8 @@ let xlate_using = function
 let xlate_one_unfold_block = function
     ([],qid) -> CT_coerce_ID_to_UNFOLD(tac_qualid_to_ct_ID qid)
   | (n::nums, qid) ->
-      CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_to_int_ne_list n nums);;
+      CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_or_var_to_int_ne_list n nums)
+;;
 
 let xlate_with_names = function
     IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
@@ -728,7 +738,7 @@ and xlate_red_tactic =
       CT_simpl 
 	(CT_coerce_PATTERN_to_PATTERN_OPT
 	   (CT_pattern_occ
-	      (CT_int_list(List.map (fun n -> CT_int n) l), xlate_formula c)))
+	      (CT_int_list(nums_or_var_to_int_list_aux l), xlate_formula c)))
   | Cbv flag_list ->
      let conv_flags, red_ids = get_flag flag_list in
      CT_cbv (CT_conversion_flag_list conv_flags, red_ids)
@@ -745,7 +755,7 @@ and xlate_red_tactic =
   | Pattern l ->
      let pat_list = List.map (fun (nums,c) ->
           CT_pattern_occ
-           (CT_int_list (List.map (fun x -> CT_int x) nums),
+           (CT_int_list (nums_or_var_to_int_list_aux nums),
             xlate_formula c)) l in
      (match pat_list with
       | first :: others -> CT_pattern (CT_pattern_ne_list (first, others))
@@ -903,7 +913,7 @@ and xlate_tac =
     | TacChange (Some(l,c), f, b) -> 
 	(* TODO LATER: combine with other constructions of pattern_occ *)
 	CT_change_local(
-	  CT_pattern_occ(CT_int_list(List.map (fun n -> CT_int n) l), 
+	  CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l), 
 			 xlate_formula c),
 	  xlate_formula f,
 	  xlate_clause b)
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 6cee54e2da..f35b457a58 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -204,7 +204,7 @@ let protect_tac =
   Tactics.reduct_option (protect_red,DEFAULTcast) None ;;
 
 let protect_tac_in id =
-  Tactics.reduct_option (protect_red,DEFAULTcast) (Some(id,[],InHyp));;
+  Tactics.reduct_option (protect_red,DEFAULTcast) (Some(([],id),InHyp));;
 
 
 TACTIC EXTEND protect_fv
@@ -442,10 +442,10 @@ let add_theory name rth eqth morphth cst_tac =
     | None ->
         (match kind with
             Some true ->
-              let t = Genarg.ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
+              let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
           | Some false ->
-              let t = Genarg.ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
           | _ -> error"a tactic must be specified for an almost_ring") in
   let _ =
@@ -495,7 +495,7 @@ let ring gl =
          spc()++str"\""++pr_constr req++str"\"") in
   Tacinterp.eval_tactic
     (TacArg(TacCall(dummy_loc,
-      Genarg.ArgArg(dummy_loc, Lazy.force ltac_setoid_ring),
+      ArgArg(dummy_loc, Lazy.force ltac_setoid_ring),
       Tacexp e.ring_cst_tac::
       List.map carg [e.ring_lemma1;e.ring_lemma2;e.ring_req])))
     gl
@@ -512,7 +512,7 @@ let ring_rewrite rl =
     (lapp coq_nil [|ty|]) in
   Tacinterp.eval_tactic
     (TacArg(TacCall(dummy_loc,
-      Genarg.ArgArg(dummy_loc, Lazy.force ltac_setoid_ring_rewrite),
+      ArgArg(dummy_loc, Lazy.force ltac_setoid_ring_rewrite),
       Tacexp e.ring_cst_tac::List.map carg [e.ring_lemma2;e.ring_req;rl])))
 
 let setoid_ring = function