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

29 files changed, 157 insertions, 130 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
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 2c38b4c79d..2d51e2a183 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -44,7 +44,6 @@ type argument_type =
   | PairArgType of argument_type * argument_type
   | ExtraArgType of string
 
-type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a and_short_name = 'a * identifier located option
 type rawconstr_and_expr = rawconstr * constr_expr option
 
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 858457e3f7..dacafc4571 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -16,7 +16,6 @@ open Rawterm
 open Topconstr
 open Term
 
-type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a and_short_name = 'a * identifier located option
 
 (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 60a00df3df..fc5fc82f7e 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -23,7 +23,7 @@ type let_clause_kind =
   | LETCLAUSE of
       (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
 
-let fail_default_value = Genarg.ArgArg 0
+let fail_default_value = ArgArg 0
 
 let out_letin_clause loc = function
   | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index dd04506ca1..9a4995c03a 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -121,8 +121,8 @@ GEXTEND Gram
   simple_intropattern;
 
   int_or_var:
-    [ [ n = integer  -> Genarg.ArgArg n
-      | id = identref -> Genarg.ArgVar id ] ]
+    [ [ n = integer  -> Rawterm.ArgArg n
+      | id = identref -> Rawterm.ArgVar id ] ]
   ;
   (* An identifier or a quotation meta-variable *)
   id_or_meta:
@@ -155,11 +155,11 @@ GEXTEND Gram
   conversion:
     [ [ c = constr -> (None, c)
       | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2)
-      | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr ->
+      | c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr ->
 	  (Some (nl,c1), c2) ] ]
   ;
   occurrences:
-    [ [ "at"; nl = LIST1 integer -> nl
+    [ [ "at"; nl = LIST1 int_or_var -> nl
       | -> [] ] ]
   ;
   pattern_occ:
@@ -240,7 +240,7 @@ GEXTEND Gram
     ] ]
   ;
   hypident_occ:
-    [ [ (id,l)=hypident; occs=occurrences -> (id,occs,l) ] ]
+    [ [ (id,l)=hypident; occs=occurrences -> ((occs,id),l) ] ]
   ;
   clause:
     [ [ "in"; "*"; occs=occurrences ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 9a6f379b3a..e51b1fecba 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -153,8 +153,8 @@ let pr_lname = function
   | lna -> pr_located pr_name lna
 
 let pr_or_var pr = function
-  | Genarg.ArgArg x -> pr x
-  | Genarg.ArgVar (loc,s) -> pr_lident (loc,s)
+  | ArgArg x -> pr x
+  | ArgVar (loc,s) -> pr_lident (loc,s)
 
 let pr_prim_token = function
   | Numeral n -> Bigint.pr_bigint n
@@ -625,15 +625,10 @@ let pr_cases_pattern_expr = pr_patt ltop
 
 let pr_binders = pr_undelimited_binders (pr ltop)
 
-let pr_pattern_occ prc = function
-    ([],c) -> prc c
-  | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++
-                     hov 0 (prlist_with_sep spc int nl))
-
-let pr_unfold_occ pr_ref = function
-    ([],qid) -> pr_ref qid
-  | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++
-                       hov 0 (prlist_with_sep spc int nl))
+let pr_with_occurrences pr = function
+    ([],c) -> pr c
+  | (nl,c) -> hov 1 (pr c ++ spc() ++ str"at " ++
+                     hov 0 (prlist_with_sep spc (pr_or_var int) nl))
 
 let pr_red_flag pr r =
   (if r.rBeta then pr_arg str "beta" else mt ()) ++
@@ -653,7 +648,7 @@ let pr_metaid id = str"?" ++ pr_id id
 let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | Red false -> str "red"
   | Hnf -> str "hnf"
-  | Simpl o -> str "simpl" ++ pr_opt (pr_pattern_occ pr_constr) o  
+  | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o  
   | Cbv f ->
       if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
 	str "compute"
@@ -663,11 +658,11 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
       hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
   | Unfold l ->
       hov 1 (str "unfold" ++ spc() ++
-             prlist_with_sep pr_coma (pr_unfold_occ pr_ref) l)
+             prlist_with_sep pr_coma (pr_with_occurrences pr_ref) l)
   | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l)
   | Pattern l ->
       hov 1 (str "pattern" ++
-        pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l)
+        pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l)
         
   | Red true -> error "Shouldn't be accessible from user"
   | ExtraRedExpr s -> str s
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index e7e8a4bbc0..1cafe28005 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -53,11 +53,13 @@ val pr_id : identifier -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
 
+val pr_with_occurrences :
+  ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
 val pr_red_expr :
-  ('a -> std_ppcmds) * ('a -> std_ppcmds) *  ('b -> std_ppcmds) ->
+  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) ->
     ('a,'b) red_expr_gen -> std_ppcmds
 val pr_may_eval :
-  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> 
     ('a,'b) may_eval -> std_ppcmds
 
 val pr_rawsort : rawsort -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d5a94cd179..2f86ac94cf 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -142,8 +142,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
   | SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x)
   | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
   | ConstrMayEvalArgType ->
-      pr_arg (pr_may_eval prc prlc prref)
-        (out_gen rawwit_constr_may_eval x)
+      pr_arg (pr_may_eval prc prlc prref) (out_gen rawwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
   | RedExprArgType ->
@@ -186,7 +185,8 @@ let rec pr_glob_generic prc prlc prtac x =
   | ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
   | ConstrMayEvalArgType ->
       pr_arg (pr_may_eval prc prlc
-        (pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_constr_may_eval x)
+        (pr_or_var (pr_and_short_name pr_evaluable_reference)))
+        (out_gen globwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
   | RedExprArgType ->
@@ -381,17 +381,14 @@ let pr_by_tactic prt = function
   | TacId [] -> mt ()
   | tac -> spc() ++ str "by " ++ prt tac
 
-let pr_occs pp = function
-    [] -> pp
-  | nl -> hov 1 (pp ++ spc() ++ str"at " ++
-                 hov 0 (prlist_with_sep spc int nl))
-
 let pr_hyp_location pr_id = function
-  | id, occs, InHyp -> spc () ++ pr_occs (pr_id id) occs
-  | id, occs, InHypTypeOnly ->
-      spc () ++ pr_occs (str "(type of " ++ pr_id id ++ str ")") occs
-  | id, occs, InHypValueOnly ->
-      spc () ++ pr_occs (str "(value of " ++ pr_id id ++ str ")") occs
+  | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+  | occs, InHypTypeOnly ->
+      spc () ++ 
+      pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
+  | occs, InHypValueOnly ->
+      spc () ++ 
+      pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
 
 let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
 
@@ -401,11 +398,11 @@ let pr_simple_clause pr_id = function
 
 let pr_clauses pr_id = function
     { onhyps=None; onconcl=true; concl_occs=nl } ->
-      pr_in (pr_occs (str " *") nl)
+      pr_in (pr_with_occurrences (fun () -> str " *") (nl,()))
   | { onhyps=None; onconcl=false } -> pr_in (str " * |-")
   | { onhyps=Some l; onconcl=true; concl_occs=nl } -> 
       pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l
-             ++ pr_occs (str" |- *") nl)
+             ++ pr_with_occurrences (fun () -> str" |- *") (nl,()))
   | { onhyps=Some l; onconcl=false } ->
       pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l)
 
@@ -779,7 +776,8 @@ and pr_atom1 env = function
         | Some([],c1) -> hov 1 (pr_constr env c1 ++ spc() ++ str "with ")
         | Some(ocl,c1) ->
             hov 1 (pr_constr env c1 ++ spc() ++
-	           str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++
+	           str "at " ++ prlist_with_sep spc (pr_or_var int) ocl) ++
+                   spc() ++
 	           str "with ") ++
       pr_constr env c ++ pr_clauses pr_ident h)
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index b05895666f..2cc30f5edd 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -77,20 +77,22 @@ let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
 let mlexpr_of_loc loc = <:expr< $dloc$ >>
 
 let mlexpr_of_or_var f = function
-  | Genarg.ArgArg x -> <:expr< Genarg.ArgArg $f x$ >>
-  | Genarg.ArgVar id -> <:expr< Genarg.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
+  | Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >>
+  | Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
 
 let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
 
-let mlexpr_of_occs = mlexpr_of_list mlexpr_of_int
+let mlexpr_of_occs = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int)
+
+let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
 
 let mlexpr_of_hyp_location = function
-  | id, occs, Tacexpr.InHyp ->
-      <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHyp) >>
-  | id, occs, Tacexpr.InHypTypeOnly ->
-      <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypTypeOnly) >>
-  | id, occs, Tacexpr.InHypValueOnly ->
-      <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypValueOnly) >>
+  | occs, Tacexpr.InHyp ->
+      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHyp) >>
+  | occs, Tacexpr.InHypTypeOnly ->
+      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypTypeOnly) >>
+  | occs, Tacexpr.InHypValueOnly ->
+      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypValueOnly) >>
 
 let mlexpr_of_clause cl =
   <:expr< {Tacexpr.onhyps=
@@ -140,7 +142,8 @@ let rec mlexpr_of_constr = function
   | _ -> failwith "mlexpr_of_constr: TODO"
 
 let mlexpr_of_occ_constr =
-  mlexpr_of_pair (mlexpr_of_list mlexpr_of_int) mlexpr_of_constr
+  mlexpr_of_pair (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int))
+    mlexpr_of_constr
 
 let mlexpr_of_red_expr = function
   | Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >>
@@ -151,7 +154,7 @@ let mlexpr_of_red_expr = function
   | Rawterm.Lazy f ->
       <:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >>
   | Rawterm.Unfold l ->
-      let f1 = mlexpr_of_list mlexpr_of_int in
+      let f1 = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) in
       let f2 = mlexpr_of_reference in
       let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in
       <:expr< Rawterm.Unfold $f l$ >>
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 480ee13b2b..9a0e51e108 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -263,22 +263,24 @@ type 'a raw_red_flag = {
 let all_flags =
   {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
 
-type 'a occurrences = int list * 'a
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+
+type 'a with_occurrences = int or_var list * 'a
 
 type ('a,'b) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a occurrences option
+  | Simpl of 'a with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
-  | Unfold of 'b occurrences list
+  | Unfold of 'b with_occurrences list
   | Fold of 'a list
-  | Pattern of 'a occurrences list
+  | Pattern of 'a with_occurrences list
   | ExtraRedExpr of string
   | CbvVm
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a, 'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d64ba03a79..f6541ff314 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -132,22 +132,24 @@ type 'a raw_red_flag = {
 
 val all_flags : 'a raw_red_flag
 
-type 'a occurrences = int list * 'a
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+
+type 'a with_occurrences = int or_var list * 'a
 
 type ('a,'b) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a occurrences option
+  | Simpl of 'a with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
-  | Unfold of 'b occurrences list
+  | Unfold of 'b with_occurrences list
   | Fold of 'a list
-  | Pattern of 'a occurrences list
+  | Pattern of 'a with_occurrences list
   | ExtraRedExpr of string
   | CbvVm
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a, 'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 9ffa1dfb76..84cc87e7f0 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -77,5 +77,5 @@ val reduce_to_quantified_ref :
 val reduce_to_atomic_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
-val contextually : bool -> constr occurrences -> reduction_function
+val contextually : bool -> int list * constr -> reduction_function
   -> reduction_function
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 2fed1cd2c3..6f49ee7353 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -93,19 +93,26 @@ let declare_red_expr s f =
   with Not_found ->
     red_expr_tab := Stringmap.add s f !red_expr_tab
 
+let out_arg = function
+  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgArg x -> x
+
+let out_with_occurrences (l,c) =
+  (List.map out_arg l, c)
+
 let reduction_of_red_expr = function
   | Red internal -> 
       if internal then (try_red_product,DEFAULTcast) 
       else (red_product,DEFAULTcast)
   | Hnf -> (hnf_constr,DEFAULTcast)
-  | Simpl (Some (_,c as lp)) -> 
-      (contextually (is_reference c) lp nf,DEFAULTcast)
+  | Simpl (Some (_,c as lp)) ->
+      (contextually (is_reference c) (out_with_occurrences lp) nf,DEFAULTcast)
   | Simpl None -> (nf,DEFAULTcast)
   | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
   | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
-  | Unfold ubinds -> (unfoldn ubinds,DEFAULTcast)
+  | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)
   | Fold cl -> (fold_commands cl,DEFAULTcast)
-  | Pattern lp -> (pattern_occs lp,DEFAULTcast)
+  | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
   | ExtraRedExpr s ->
       (try (Stringmap.find s !red_expr_tab,DEFAULTcast)
       with Not_found -> error("unknown user-defined reduction \""^s^"\""))
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 1c9393d7fa..fee3f98132 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -17,6 +17,8 @@ open Reductionops
 
 type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
+val out_with_occurrences : 'a with_occurrences -> int list * 'a
+
 val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
 (* [true] if we should use the vm to verify the reduction *)
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 89060f9ccc..af3eec9812 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -56,7 +56,7 @@ type hyp_location_flag = (* To distinguish body and type of local defs *)
   | InHypTypeOnly
   | InHypValueOnly
 
-type 'a raw_hyp_location = 'a * int list * hyp_location_flag
+type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
 
 type 'a induction_arg =
   | ElimOnConstr of 'a
@@ -80,6 +80,7 @@ type 'id message_token =
   | MsgInt of int
   | MsgIdent of 'id
 
+
 type 'id gsimple_clause = ('id raw_hyp_location) option
 (* onhyps:
      [None] means *on every hypothesis*
@@ -87,7 +88,7 @@ type 'id gsimple_clause = ('id raw_hyp_location) option
 type 'id gclause =
   { onhyps : 'id raw_hyp_location list option;
     onconcl : bool;
-    concl_occs :int list }
+    concl_occs : int or_var list }
 
 let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
 
@@ -175,8 +176,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
   (* Conversion *)
   | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause
-  | TacChange of
-      'constr occurrences option * 'constr * 'id gclause
+  | TacChange of 'constr with_occurrences option * 'constr * 'id gclause
 
   (* Equivalence relations *)
   | TacReflexivity
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f7ae4311c7..1ecb29f7e4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -778,7 +778,7 @@ let gen_auto n lems dbnames =
   | None -> full_auto n lems
   | Some l -> auto n lems l
 
-let inj_or_var = option_map (fun n -> Genarg.ArgArg n)
+let inj_or_var = option_map (fun n -> ArgArg n)
 
 let h_auto n lems l =
   Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l)
@@ -849,7 +849,7 @@ let compileAutoArg contac = function
       (tclTHEN  
          (Tacticals.tryAllClauses 
             (function 
-               | Some (id,_,_) -> Dhyp.h_destructHyp false id
+               | Some ((_,id),_) -> Dhyp.h_destructHyp false id
                | None          -> Dhyp.h_destructConcl))
          contac)
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index cd8a59136a..b1eecef3f2 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -265,10 +265,10 @@ let match_dpat dp cls gls =
     | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) ->
         let hl = match lo with
             Some l -> l
-          | None -> List.map (fun id -> (id,[],InHyp)) (pf_ids_of_hyps gls) in
+          | None -> List.map (fun id -> (([],id),InHyp)) (pf_ids_of_hyps gls) in
         if not
           (List.for_all
-            (fun (id,_,hl) ->
+            (fun ((_,id),hl) ->
               let cltyp = pf_get_hyp_typ gls id in
               let cl = pf_concl gls in
               (hl=InHyp) &
@@ -297,7 +297,7 @@ let applyDestructor cls discard dd gls =
   let tacl =
     List.map (fun cl ->
       match cl, dd.d_code with
-        | Some (id,_,_), (Some x, tac) -> 
+        | Some ((_,id),_), (Some x, tac) -> 
 	    let arg =
               ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in
             TacLetIn ([(dummy_loc, x), None, arg], tac)
@@ -308,7 +308,7 @@ let applyDestructor cls discard dd gls =
   let discard_0 =
     List.map (fun cl ->
       match (cl,dd.d_pat) with
-        | (Some (id,_,_),HypLocation(discardable,_,_)) ->
+        | (Some ((_,id),_),HypLocation(discardable,_,_)) ->
             if discard & discardable then thin [id] else tclIDTAC
         | (None,ConclLocation _) -> tclIDTAC
         | _ -> error "ApplyDestructor" ) cll in
@@ -356,7 +356,7 @@ let rec search n =
      (tclTHEN  
         (Tacticals.tryAllClauses 
            (function 
-              | Some (id,_,_) -> (dHyp id)
+              | Some ((_,id),_) -> (dHyp id)
               | None    ->  dConcl ))
         (search (n-1)))]
     
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 598a6fe0ae..66de55a1d8 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -149,7 +149,7 @@ let rec prolog l n gl =
 let prolog_tac l n gl =
   let n =
     match n with
-      |  Genarg.ArgArg n -> n
+      |  ArgArg n -> n
       | _ -> error "Prolog called with a non closed argument"
   in
   try (prolog l n gl)
@@ -383,12 +383,12 @@ let gen_eauto d np lems = function
 
 let make_depth = function
   | None -> !default_search_depth 
-  | Some (Genarg.ArgArg d) -> d
+  | Some (ArgArg d) -> d
   | _ -> error "EAuto called with a non closed argument"
 
 let make_dimension n = function
   | None -> (true,make_depth n)
-  | Some (Genarg.ArgArg d) -> (false,d)
+  | Some (ArgArg d) -> (false,d)
   | _ -> error "EAuto called with a non closed argument"
 
 open Genarg
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 34cfefd5d4..ea7967bb1d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -123,7 +123,7 @@ let general_rewrite_in l2r id c =
 let general_multi_rewrite l2r c cl = 
   let rec do_hyps = function 
     | [] -> tclIDTAC
-    | (id,_,_) :: l -> 
+    | ((_,id),_) :: l -> 
 	tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
   in 
   let rec try_do_hyps = function 
@@ -523,7 +523,7 @@ let onNegatedEquality tac gls =
 
 let discrSimpleClause = function
   | None -> onNegatedEquality discrEq
-  | Some (id,_,_) -> onEquality discrEq id
+  | Some ((_,id),_) -> onEquality discrEq id
 
 let discr = onEquality discrEq
 
@@ -1060,7 +1060,7 @@ let unfold_body x gl =
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis") in
   let aft = afterHyp x gl in
-  let hl = List.fold_right (fun (y,yval,_) cl -> (y,[],InHyp) :: cl) aft [] in
+  let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 11bb71ca8c..a6155598cd 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -58,7 +58,7 @@ fun prc _ _ opt_c->
     | Some c -> 
 	spc () ++ hov 2 (str "by" ++ spc () ++ 
 			   Pptactic.pr_or_var (fun _ -> mt ()) 
-			   (ArgVar(Util.dummy_loc,c))
+			   (Rawterm.ArgVar(Util.dummy_loc,c))
 			)
 
 
@@ -76,7 +76,7 @@ ARGUMENT EXTEND in_arg_hyp
   PRINTED BY pr_in_arg_hyp
 | [ "in" int_or_var(c) ] -> 
     [ match c with
-	| ArgVar(_,c) ->  Some (c)
+	| Rawterm.ArgVar(_,c) ->  Some (c)
 	| _ -> Util.error "in must be used with an identifier" 
     ]
 | [ ] -> [ None ]
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index e0fd138c2b..02792cb331 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -88,7 +88,9 @@ let h_simplest_right  = h_right NoBindings
 
 (* Conversion *)
 let h_reduce r cl  = abstract_tactic (TacReduce (r,cl)) (reduce r cl)
-let h_change oc c cl  = abstract_tactic (TacChange (oc,c,cl)) (change oc c cl)
+let h_change oc c cl =
+  abstract_tactic (TacChange (oc,c,cl))
+    (change (option_map Redexpr.out_with_occurrences oc) c cl)
 
 (* Equivalence relations *)
 let h_reflexivity    = abstract_tactic TacReflexivity intros_reflexivity
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 15bea4bb3a..2823a53ad5 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -89,7 +89,7 @@ val h_simplest_right  : tactic
 (* Conversion *)
 val h_reduce          : Redexpr.red_expr -> Tacticals.clause -> tactic
 val h_change          :
-  constr occurrences option -> constr -> Tacticals.clause -> tactic
+  constr with_occurrences option -> constr -> Tacticals.clause -> tactic
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ed9a4ecf8f..20ca5dc93f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -529,8 +529,8 @@ let intern_inversion_strength lf ist = function
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
 
 (* Interprets an hypothesis name *)
-let intern_hyp_location ist (id,occs,hl) =
-  (intern_hyp ist (skip_metaid id), occs, hl)
+let intern_hyp_location ist ((occs,id),hl) =
+  ((List.map (intern_int_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl)
 
 let interp_constrpattern_gen sigma env ltacvar c =
   let c = intern_gen false ~allow_soapp:true ~ltacvars:(ltacvar,[])
@@ -1124,7 +1124,9 @@ let interp_evaluable ist env = function
   | ArgVar (_,id) -> coerce_to_evaluable_ref env (List.assoc id ist.lfun)
 
 (* Interprets an hypothesis name *)
-let interp_hyp_location ist gl (id,occs,hl) = (interp_hyp ist gl id,occs,hl)
+let interp_hyp_location ist gl ((occs,id),hl) =
+  ((List.map (fun n -> ArgArg (interp_int_or_var ist n)) occs,
+    interp_hyp ist gl id),hl)
 
 let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
   { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol;
@@ -1264,7 +1266,9 @@ let interp_unfold ist env (l,qid) =
 let interp_flag ist env red =
   { red with rConst = List.map (interp_evaluable ist env) red.rConst }
 
-let interp_pattern ist sigma env (l,c) = (l,interp_constr ist sigma env c)
+let interp_pattern ist sigma env (l,c) = 
+  (List.map (fun n -> ArgArg (interp_int_or_var ist n)) l,
+   interp_constr ist sigma env c)
 
 let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl)
 
@@ -1945,7 +1949,7 @@ let subst_and_short_name f (c,n) =
 
 let subst_or_var f =  function
   | ArgVar _ as x -> x
-  | ArgArg (x) -> ArgArg (f x)
+  | ArgArg x -> ArgArg (f x)
 
 let subst_located f (_loc,id) = (loc,f id)
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3b5349a4bd..c5cf54d47b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -119,13 +119,13 @@ type clause = identifier gclause
 
 let allClauses = { onhyps=None; onconcl=true; concl_occs=[] }
 let allHyps = { onhyps=None; onconcl=false; concl_occs=[] }
-let onHyp id = { onhyps=Some[(id,[],InHyp)]; onconcl=false; concl_occs=[] }
+let onHyp id = { onhyps=Some[(([],id),InHyp)]; onconcl=false; concl_occs=[] }
 let onConcl = { onhyps=Some[]; onconcl=true; concl_occs=[] }
 
 let simple_clause_list_of cl gls =
   let hyps =
     match cl.onhyps with 
-        None -> List.map (fun id -> Some(id,[],InHyp)) (pf_ids_of_hyps gls)
+        None -> List.map (fun id -> Some(([],id),InHyp)) (pf_ids_of_hyps gls)
       | Some l -> List.map (fun h -> Some h) l in
   if cl.onconcl then None::hyps else hyps
 
@@ -167,7 +167,7 @@ let nth_clause n gl =
 let clause_type cls gl =
   match simple_clause_of cls with
     | None    -> pf_concl gl
-    | Some (id,_,_) -> pf_get_hyp_typ gl id
+    | Some ((_,id),_) -> pf_get_hyp_typ gl id
 
 (* Functions concerning matching of clausal environments *)
 
@@ -217,7 +217,7 @@ let onAllClausesLR tac = onClausesLR tac allClauses
 let onNthLastHyp n tac gls = tac (nth_clause n gls) gls
 
 let tryAllHyps     tac =
-  tryClauses (function Some(id,_,_) -> tac id | _ -> assert false) allHyps
+  tryClauses (function Some((_,id),_) -> tac id | _ -> assert false) allHyps
 let onNLastHyps n  tac     = onHyps (nLastHyps n) (tclMAP tac)
 let onLastHyp      tac gls = tac (lastHyp gls) gls
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b86562493d..fa9c2ed236 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -147,7 +147,7 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 let reduct_in_concl (redfun,sty) gl = 
   convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
 
-let reduct_in_hyp redfun (id,_,where) gl =
+let reduct_in_hyp redfun ((_,id),where) gl =
   let (_,c, ty) = pf_get_hyp gl id in
   let redfun' = (*under_casts*) (pf_reduce redfun gl) in
   match c with
@@ -967,19 +967,21 @@ let quantify lconstr =
    the left of each x1, ...).
 *)
 
-
+let out_arg = function
+  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgArg x -> x
 
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
       [] -> None
-    | (id',occs,hl)::_ when id=id' -> Some occs
+    | ((occs,id'),hl)::_ when id=id' -> Some (List.map out_arg occs)
     | _::l -> hyp_occ l in
   match cls.onhyps with
       None -> Some []
     | Some l -> hyp_occ l
 
 let occurrences_of_goal cls =
-  if cls.onconcl then Some cls.concl_occs else None
+  if cls.onconcl then Some (List.map out_arg cls.concl_occs) else None
 
 let in_every_hyp cls = (cls.onhyps=None)
 
@@ -2004,7 +2006,7 @@ let unfold_body x gl =
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis") in
   let aft = afterHyp x gl in
-  let hl = List.fold_right (fun (y,yval,_) cl -> (y,[],InHyp) :: cl) aft [] in
+  let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
@@ -2191,7 +2193,7 @@ let dAnd cls =
   onClauses
     (function
       | None    -> simplest_split
-      | Some (id,_,_) -> andE id)
+      | Some ((_,id),_) -> andE id)
     cls
 
 let orE id gl =
@@ -2205,7 +2207,7 @@ let orE id gl =
 let dorE b cls =
   onClauses
     (function
-      | (Some (id,_,_)) -> orE id
+      | (Some ((_,id),_)) -> orE id
       |  None     -> (if b then right else left) NoBindings)
     cls
 
@@ -2225,7 +2227,7 @@ let dImp cls =
   onClauses
     (function
       | None    -> intro
-      | Some (id,_,_) -> impE id)
+      | Some ((_,id),_) -> impE id)
     cls
 
 (************************************************)
@@ -2300,7 +2302,7 @@ let intros_symmetry =
   onClauses
     (function
       | None -> tclTHEN intros symmetry
-      | Some (id,_,_) -> symmetry_in id)
+      | Some ((_,id),_) -> symmetry_in id)
 
 (* Transitivity tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 79dd4d291e..f5355eba13 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -115,8 +115,8 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
 val reduct_option     : tactic_reduction * cast_kind -> simple_clause -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
-val change_in_concl   : constr occurrences option -> constr -> tactic
-val change_in_hyp     : constr occurrences option -> constr -> hyp_location ->
+val change_in_concl   : (int list * constr) option -> constr -> tactic
+val change_in_hyp     : (int list * constr) option -> constr -> hyp_location ->
   tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location        -> tactic
@@ -139,7 +139,7 @@ val unfold_option     :
     -> tactic
 val reduce            : red_expr -> clause -> tactic
 val change            :
-  constr occurrences option -> constr -> clause -> tactic
+  (int list * constr) option -> constr -> clause -> tactic
 
 val unfold_constr     : global_reference -> tactic
 val pattern_option  : (int list * constr) list -> simple_clause -> tactic