In "simpl c" and "change c with d", c can be a pattern.

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

5 files changed, 81 insertions, 36 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0e4091b3c..8447dfdef 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -273,7 +273,7 @@ let make_exact_entry sigma pri (c,cty) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = Pattern.pattern_of_constr sigma cty in
+	let pat = snd (Pattern.pattern_of_constr sigma cty) in
 	let head = 
 	  try head_of_constr_reference (fst (head_constr cty)) 
 	  with _ -> failwith "make_exact_entry" 
@@ -287,7 +287,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = Pattern.pattern_of_constr sigma c' in
+	let pat = snd (Pattern.pattern_of_constr sigma c') in
         let hd = (try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry") in
         let nmiss = List.length (clenv_missing ce) in
@@ -354,7 +354,7 @@ let make_trivial env sigma c =
   let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
   (Some hd, { pri=1;
-         pat = Some (Pattern.pattern_of_constr sigma (clenv_type ce));
+         pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce)));
          code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
 
 open Vernacexpr
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 70eb8dfb3..d649c8b31 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -108,7 +108,8 @@ val h_simplest_right  : tactic
 (* Conversion *)
 val h_reduce          : Redexpr.red_expr -> Tacticals.clause -> tactic
 val h_change          :
-  constr with_occurrences option -> constr -> Tacticals.clause -> tactic
+  Pattern.constr_pattern with_occurrences option -> constr -> 
+    Tacticals.clause -> tactic
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f031df256..719fa7f85 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -575,13 +575,27 @@ let intern_flag ist red =
 
 let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
 
+let intern_constr_pattern ist ltacvars pc =
+  let metas,pat =
+    Constrintern.intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in
+  let c = intern_constr_gen true false ist pc in
+  metas,(c,pat)
+
+let intern_typed_pattern_with_occurrences ist (l,p) =
+  let c = intern_constr_gen true false ist p in
+  (* we cannot ensure in non strict mode that the pattern is closed *)
+  (* keeping a constr_expr copy is too complicated and we want anyway to *)
+  (* type it, so we remember the pattern as a rawconstr only *)
+  let dummy_pat = PRel 0 in
+  (l,(c,dummy_pat))
+
 let intern_red_expr ist = function
   | Unfold l -> Unfold (List.map (intern_unfold ist) l)
   | Fold l -> Fold (List.map (intern_constr ist) l)
   | Cbv f -> Cbv (intern_flag ist f)
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
-  | Simpl o -> Simpl (Option.map (intern_constr_with_occurrences ist) o)
+  | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
 
 let intern_in_hyp_as ist lf (id,ipat) =
@@ -607,14 +621,12 @@ let intern_hyp_location ist (((b,occs),id),hl) =
 let intern_pattern ist ?(as_type=false) lfun = function
   | Subterm (b,ido,pc) ->
       let ltacvars = (lfun,[]) in
-      let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in
-      let c = intern_constr_gen true false ist pc in
-      ido, metas, Subterm (b,ido,(c,pat))
+      let (metas,pc) = intern_constr_pattern ist ltacvars pc in
+      ido, metas, Subterm (b,ido,pc)
   | Term pc ->
       let ltacvars = (lfun,[]) in
-      let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~as_type ~ltacvars pc in
-      let c = intern_constr_gen true false ist pc in
-      None, metas, Term (c,pat)
+      let (metas,pc) = intern_constr_pattern ist ltacvars pc in
+      None, metas, Term pc
 
 let intern_constr_may_eval ist = function
   | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
@@ -782,13 +794,17 @@ let rec intern_atomic lf ist x =
   (* Conversion *)
   | TacReduce (r,cl) ->
       TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
-  | TacChange (occl,c,cl) ->
-      TacChange (Option.map (intern_constr_with_occurrences ist) occl,
-        (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
+  | TacChange (None,c,cl) ->
+      TacChange (None,
+        (if (cl.onhyps = None or cl.onhyps = Some []) &
 	    (cl.concl_occs = all_occurrences_expr or
 	     cl.concl_occs = no_occurrences_expr)
          then intern_type ist c else intern_constr ist c),
 	clause_app (intern_hyp_location ist) cl)
+  | TacChange (Some occl,c,cl) ->
+      let occl = intern_typed_pattern_with_occurrences ist occl in
+      TacChange (Some occl,intern_constr ist c,
+	clause_app (intern_hyp_location ist) cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> TacReflexivity
@@ -1314,7 +1330,7 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
   (* Side-effect *)
   !evdref,c
 
-let interp_gen kind ist expand_evar fail_evar use_classes env sigma (c,ce) =
+let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma (c,ce) =
   let (ltacvars,unbndltacvars as vars),typs =
     extract_ltac_vars_data ist sigma env in
   let c = match ce with
@@ -1324,7 +1340,8 @@ let interp_gen kind ist expand_evar fail_evar use_classes env sigma (c,ce) =
        intros/lettac/inversion hypothesis names *)
   | Some c ->
       let ltacdata = (List.map fst ltacvars,unbndltacvars) in
-      intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in
+      intern_gen (kind = IsType) ~allow_patvar ~ltacvars:ltacdata sigma env c
+  in
   let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
   let evd,c =
     catch_error trace
@@ -1339,20 +1356,22 @@ let interp_gen kind ist expand_evar fail_evar use_classes env sigma (c,ce) =
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
-  snd (interp_gen kind ist true true true env sigma c)
+  snd (interp_gen kind ist false true true true env sigma c)
 
 let interp_constr = interp_constr_gen (OfType None)
 
 let interp_type = interp_constr_gen IsType
 
 (* Interprets an open constr *)
-let interp_open_constr_gen kind ist = interp_gen kind ist true false false
+let interp_open_constr_gen kind ist =
+  interp_gen kind ist false true false false
 
 let interp_open_constr ccl =
   interp_open_constr_gen (OfType ccl)
 
 let interp_typed_pattern ist env sigma c =
-  let sigma, c = interp_gen (OfType None) ist false false false env sigma c in
+  let sigma, c =
+    interp_gen (OfType None) ist true false false false env sigma c in
   pattern_of_constr sigma c
 
 (* Interprets a constr expression casted by the current goal *)
@@ -1402,11 +1421,15 @@ let interp_unfold ist env (occs,qid) =
 let interp_flag ist env red =
   { red with rConst = List.map (interp_evaluable ist env) red.rConst }
 
-let interp_pattern ist sigma env (occs,c) =
+let interp_constr_with_occurrences ist sigma env (occs,c) =
   (interp_occurrences ist occs, interp_constr ist sigma env c)
 
-let pf_interp_constr_with_occurrences ist gl =
-  interp_pattern ist (pf_env gl) (project gl)
+let interp_typed_pattern_with_occurrences ist env sigma (occs,(c,_)) =
+  let sign,p = interp_typed_pattern ist env sigma c in
+  sign, (interp_occurrences ist occs, p)
+
+let interp_closed_typed_pattern_with_occurrences ist env sigma occl =
+  snd (interp_typed_pattern_with_occurrences ist env sigma occl)
 
 let interp_constr_with_occurrences_and_name_as_list =
   interp_constr_in_compound_list
@@ -1414,7 +1437,7 @@ let interp_constr_with_occurrences_and_name_as_list =
     (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c
       | _ -> raise Not_found)
     (fun ist env sigma (occ_c,na) ->
-      sigma, (interp_pattern ist env sigma occ_c,
+      sigma, (interp_constr_with_occurrences ist env sigma occ_c,
        interp_fresh_name ist env na))
 
 let interp_red_expr ist sigma env = function
@@ -1422,8 +1445,10 @@ let interp_red_expr ist sigma env = function
   | Fold l -> Fold (List.map (interp_constr ist env sigma) l)
   | Cbv f -> Cbv (interp_flag ist env f)
   | Lazy f -> Lazy (interp_flag ist env f)
-  | Pattern l -> Pattern (List.map (interp_pattern ist env sigma) l)
-  | Simpl o -> Simpl (Option.map (interp_pattern ist env sigma) o)
+  | Pattern l ->
+      Pattern (List.map (interp_constr_with_occurrences ist env sigma) l)
+  | Simpl o ->
+      Simpl(Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
   | (Red _ |  Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl)
@@ -1641,9 +1666,9 @@ let use_types = false
 
 let eval_pattern lfun ist env sigma (c,pat) =
   if use_types then
-    interp_typed_pattern ist env sigma c
+    snd (interp_typed_pattern ist env sigma c)
   else
-    let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr Evd.empty c))) lfun in
+    let lvar = List.map (fun (id,c) -> (id,lazy(snd (pattern_of_constr Evd.empty c)))) lfun in
     instantiate_pattern lvar pat
 
 let read_pattern lfun ist env sigma = function
@@ -1768,6 +1793,12 @@ let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
 
 let pack_sigma (sigma,c) = {it=c;sigma=sigma}
 
+let extend_gl_hyps gl sign =
+ { gl with
+   it = { gl.it with
+     evar_hyps = 
+     List.fold_right Environ.push_named_context_val sign gl.it.evar_hyps } }
+
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist gl (tac:glob_tactic_expr) =
 
@@ -2363,14 +2394,20 @@ and interp_atomic ist gl tac =
   (* Conversion *)
   | TacReduce (r,cl) ->
       h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl)
-  | TacChange (occl,c,cl) ->
-      h_change (Option.map (pf_interp_constr_with_occurrences ist gl) occl)
-        (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
+  | TacChange (None,c,cl) ->
+      h_change None
+        (if (cl.onhyps = None or cl.onhyps = Some []) &
 	    (cl.concl_occs = all_occurrences_expr or
 	     cl.concl_occs = no_occurrences_expr)
 	 then pf_interp_type ist gl c
 	 else pf_interp_constr ist gl c)
         (interp_clause ist gl cl)
+  | TacChange (Some occl,c,cl) ->
+      let sign,occl =
+        interp_typed_pattern_with_occurrences ist env sigma occl in
+      h_change (Some occl)
+        (pf_interp_constr ist (extend_gl_hyps gl sign) c)
+        (interp_clause ist gl cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
@@ -2589,13 +2626,16 @@ let subst_flag subst red =
 
 let subst_constr_with_occurrences subst (l,c) = (l,subst_rawconstr subst c)
 
+let subst_pattern_with_occurrences subst (l,(c,p)) =
+  (l,(subst_rawconstr subst c,subst_pattern subst p))
+
 let subst_redexp subst = function
   | Unfold l -> Unfold (List.map (subst_unfold subst) l)
   | Fold l -> Fold (List.map (subst_rawconstr subst) l)
   | Cbv f -> Cbv (subst_flag subst f)
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
-  | Simpl o -> Simpl (Option.map (subst_constr_with_occurrences subst) o)
+  | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let subst_raw_may_eval subst = function
@@ -2687,7 +2727,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
   | TacChange (occl,c,cl) ->
-      TacChange (Option.map (subst_constr_with_occurrences subst) occl,
+      TacChange (Option.map (subst_pattern_with_occurrences subst) occl,
         subst_rawconstr subst c, cl)
 
   (* Equivalence relations *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 332e93c8c..4157d332b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -311,7 +311,9 @@ let change_and_check cv_pb t env sigma c =
 (* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb t = function
   | None -> change_and_check cv_pb t
-  | Some occl -> contextually false occl (change_and_check Reduction.CONV t)
+  | Some occl ->
+      contextually false occl
+        (fun subst -> change_and_check Reduction.CONV (replace_vars subst t))
 
 let change_in_concl occl t =
   reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d2cbeb856..e8662a50d 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -27,6 +27,7 @@ open Genarg
 open Tacexpr
 open Nametab
 open Rawterm
+open Pattern
 open Termops
 (*i*)
 
@@ -125,8 +126,9 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
 val reduct_option     : tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
-val change_in_concl   : (occurrences * constr) option -> constr -> tactic
-val change_in_hyp     : (occurrences * constr) option -> constr ->
+val change_in_concl   : (occurrences * constr_pattern) option -> constr -> 
+                        tactic
+val change_in_hyp     : (occurrences * constr_pattern) option -> constr ->
                         hyp_location -> tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location -> tactic
@@ -148,7 +150,7 @@ val unfold_in_hyp     :
 val unfold_option     :
   (occurrences * evaluable_global_reference) list -> goal_location -> tactic
 val change            :
-  (occurrences * constr) option -> constr -> clause -> tactic
+  (occurrences * constr_pattern) option -> constr -> clause -> tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> tactic
 val reduce            : red_expr -> clause -> tactic