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

11 files changed, 46 insertions, 38 deletions

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