Ajout Simpl et Change sur des sous-termes

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

18 files changed, 157 insertions, 119 deletions

diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 1398499cf5..9a2ff4d207 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -357,6 +357,7 @@ let my_cut c gl=
      let concl = pf_concl gl in
        apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
 ;;
+
 let exact = exact_check;;
 
 let tac_use h = match h.htype with
@@ -522,7 +523,7 @@ let rec fourier gl=
                       else tac_zero_infeq_false gl (rational_to_fraction cres)
            in
            tac:=(tclTHENS (my_cut ineq) 
-                     [tclTHEN (change_in_concl
+                     [tclTHEN (change_in_concl None
 			       (mkAppL [| parse "not"; ineq|]
 				       ))
 		      (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index d5715fd3d5..153d3f6374 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -402,7 +402,7 @@ and my_find_search db_list local_db hdc concl =
 	match t with
 	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
 	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
-	  | Give_exact c  -> exact_no_check c
+	  | Give_exact c  -> exact_check c
 	  | Res_pf_THEN_trivial_fail (term,cl) -> 
 	      tclTHEN 
 		(unify_resolve (term,cl)) 
@@ -516,7 +516,7 @@ let blast_auto = (free_try default_full_auto)
 			  (free_try (my_full_eauto 2)))
 *)
 ;;
-let blast_simpl = (free_try (reduce Simpl []))
+let blast_simpl = (free_try (reduce (Simpl None) []))
 ;;
 let blast_induction1 = 
     (free_try (tclTHEN (tclTRY intro)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 1c139ca8ea..4802933337 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -538,7 +538,8 @@ and xlate_red_tactic =
   | Red true -> xlate_error ""
   | Red false -> CT_red
   | Hnf -> CT_hnf
-  | Simpl -> CT_simpl
+  | Simpl None -> CT_simpl
+  | Simpl (Some c) -> xlate_error "Simpl: TODO"
   | Cbv flag_list ->
      let conv_flags, red_ids = get_flag flag_list in
      CT_cbv (CT_conversion_flag_list conv_flags, red_ids)
@@ -649,7 +650,8 @@ and xlate_tac =
   function
     | TacExtend (_,"Absurd",[c]) ->
        CT_absurd (xlate_formula (out_gen rawwit_constr c))
-    | TacChange (f, b) -> CT_change (xlate_formula f, xlate_clause b)
+    | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
+    | TacChange (_, f, b) -> xlate_error "TODO: Change subterms"
     | TacExtend (_,"Contradiction",[]) -> CT_contradiction
     | TacDoubleInduction (AnonHyp n1, AnonHyp n2) ->
 	CT_tac_double (CT_int n1, CT_int n2)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 341752f458..5cfc324eb7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -139,6 +139,12 @@ GEXTEND Gram
     [ [ id = base_ident -> NamedHyp id
       | n = natural -> AnonHyp n ] ]
   ;
+  conversion:
+    [ [ nl = LIST1 integer; c1 = constr; "with"; c2 = constr ->
+         (Some (nl,c1), c2)
+      |	c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2)
+      | c = constr -> (None, c) ] ]
+  ;
   pattern_occ:
     [ [ nl = LIST0 integer; c = constr -> (nl,c) ] ]
   ;
@@ -195,7 +201,7 @@ GEXTEND Gram
   red_tactic:
     [ [ IDENT "Red" -> Red false
       | IDENT "Hnf" -> Hnf
-      | IDENT "Simpl" -> Simpl
+      | IDENT "Simpl"; po = OPT pattern_occ -> Simpl po
       | IDENT "Cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "Lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
       | IDENT "Compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
@@ -207,7 +213,7 @@ GEXTEND Gram
   red_expr:
     [ [ IDENT "Red" -> Red false
       | IDENT "Hnf" -> Hnf
-      | IDENT "Simpl" -> Simpl
+      | IDENT "Simpl"; po = OPT pattern_occ -> Simpl po
       | IDENT "Cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "Lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
       | IDENT "Compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
@@ -346,7 +352,7 @@ GEXTEND Gram
       (* Conversion *)
       | r = red_tactic; cl = clause -> TacReduce (r, cl)
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
-      | IDENT "Change"; c = constr; cl = clause -> TacChange (c,cl)
+      | IDENT "Change"; (oc,c) = conversion; cl = clause -> TacChange (oc,c,cl)
 
 (* Unused ??
       | IDENT "ML"; s = string -> ExtraTactic<:ast< (MLTACTIC $s) >>
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 6571e0af8a..6c45c9e70a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -124,6 +124,9 @@ let pr_clause_pattern pr_id = function (* To check *)
 	  ++ spc () ++ pr_id id) l ++
         pr_opt (prlist_with_sep spc int) glopt
 
+let pr_subterms pr occl =
+  hov 0 (pr_occurrences pr occl ++ spc () ++ str "with")
+
 let pr_induction_arg prc = function
   | ElimOnConstr c -> prc c
   | ElimOnIdent (_,id) -> pr_id id
@@ -452,8 +455,9 @@ and pr_atom1 = function
   (* Conversion *)  
   | TacReduce (r,h) ->
       hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clause pr_ident h)
-  | TacChange (c,h) ->
-      hov 1 (str "Change" ++ brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h)
+  | TacChange (occl,c,h) ->
+      hov 1 (str "Change" ++ pr_opt (pr_subterms pr_constr) occl ++ 
+        brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h)
 
   (* Equivalence relations *)
   | (TacReflexivity | TacSymmetry) as x -> pr_atom0 x
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 5a8258cb47..bc8128fd85 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -205,10 +205,13 @@ let rec mlexpr_of_constr = function
   | Topconstr.CMeta (loc,n) -> <:expr< Topconstr.CMeta $dloc$ $mlexpr_of_int n$ >>
   | _ -> failwith "mlexpr_of_constr: TODO"
 
+let mlexpr_of_occ_constr =
+  mlexpr_of_pair (mlexpr_of_list mlexpr_of_int) mlexpr_of_constr
+
 let mlexpr_of_red_expr = function
   | Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >>
   | Rawterm.Hnf -> <:expr< Rawterm.Hnf >>
-  | Rawterm.Simpl -> <:expr< Rawterm.Simpl >>
+  | Rawterm.Simpl o -> <:expr< Rawterm.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
   | Rawterm.Cbv f ->
       <:expr< Rawterm.Cbv $mlexpr_of_red_flags f$ >>
   | Rawterm.Lazy f ->
@@ -221,8 +224,7 @@ let mlexpr_of_red_expr = function
   | Rawterm.Fold l ->
       <:expr< Rawterm.Fold $mlexpr_of_list mlexpr_of_constr l$ >>
   | Rawterm.Pattern l ->
-      let f1 = mlexpr_of_list mlexpr_of_int in
-      let f = mlexpr_of_list (mlexpr_of_pair f1 mlexpr_of_constr) in
+      let f = mlexpr_of_list mlexpr_of_occ_constr in
       <:expr< Rawterm.Pattern $f l$ >>
   | Rawterm.ExtraRedExpr (s,c) ->
       let l = mlexpr_of_constr c in
@@ -415,9 +417,10 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacReduce (r,cl) ->
       let l = mlexpr_of_list mlexpr_of_hyp_location cl in
       <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >>
-  | Tacexpr.TacChange (c,cl) ->
+  | Tacexpr.TacChange (occl,c,cl) ->
       let l = mlexpr_of_list mlexpr_of_hyp_location cl in
-      <:expr< Tacexpr.TacChange $mlexpr_of_constr c$ $l$ >>
+      let g = mlexpr_of_option mlexpr_of_occ_constr in
+      <:expr< Tacexpr.TacChange $g occl$ $mlexpr_of_constr c$ $l$ >>
 
   (* Equivalence relations *)
   | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >>
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 7fd10ef23f..9354035497 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -250,15 +250,17 @@ type 'a raw_red_flag = {
   rConst : 'a list
 }
 
+type 'a occurrences = int list * 'a
+
 type ('a,'b) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl
+  | Simpl of 'a occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
-  | Unfold of (int list * 'b) list
+  | Unfold of 'b occurrences list
   | Fold of 'a list
-  | Pattern of (int list * 'a) list
+  | Pattern of 'a occurrences list
   | ExtraRedExpr of string * 'a
 
 type 'a or_metanum = AN of 'a | MetaNum of int located
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d1c480ef72..3c2241682b 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -106,15 +106,17 @@ type 'a raw_red_flag = {
   rConst : 'a list
 }
 
+type 'a occurrences = int list * 'a
+
 type ('a,'b) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl
+  | Simpl of 'a occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
-  | Unfold of (int list * 'b) list
+  | Unfold of 'b occurrences list
   | Fold of 'a list
-  | Pattern of (int list * 'a) list
+  | Pattern of 'a occurrences list
   | ExtraRedExpr of string * 'a
 
 type 'a or_metanum = AN of 'a | MetaNum of int located
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 26a627d178..7613cd6df7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -595,6 +595,34 @@ let whd_nf env sigma c =
 
 let nf env sigma c = strong whd_nf env sigma c
 
+let contextually (locs,c) f env sigma t =
+  let maxocc = List.fold_right max locs 0 in
+  let pos = ref 1 in
+  let check = ref true in
+  let except = List.exists (fun n -> n<0) locs in
+  if except & (List.exists (fun n -> n>=0) locs) 
+  then error "mixing of positive and negative occurences"
+  else
+   let rec traverse (env,c as envc) t =
+    if locs <> [] & (not except) & (!pos > maxocc) then t
+    else
+    if eq_constr c t then
+      let r =
+	if except then 
+	  if List.mem (- !pos) locs then t else f env sigma t
+	else 
+	  if locs = [] or List.mem !pos locs then f env sigma t else t
+      in incr pos; r
+    else
+      map_constr_with_binders_left_to_right
+	(fun d (env,c) -> (push_rel d env,lift 1 c))
+        traverse envc t
+  in
+  let t' = traverse (env,c) t in
+  if locs <> [] & List.exists (fun o -> o >= !pos or o <= - !pos) locs then
+    errorlabstrm "contextually" (str "Too few occurences");
+  t'
+
 (* linear substitution (following pretty-printer) of the value of name in c.
  * n is the number of the next occurence of name.
  * ol is the occurence list to find. *)
@@ -804,7 +832,8 @@ let declare_red_expr s f =
 let reduction_of_redexp = function
   | Red internal -> if internal then internal_red_product else red_product
   | Hnf -> hnf_constr
-  | Simpl -> nf
+  | Simpl (Some lp) -> contextually lp nf
+  | Simpl None -> nf
   | Cbv f -> cbv_norm_flags (make_flag f)
   | Lazy f -> clos_norm_flags (make_flag f)
   | Unfold ubinds -> unfoldn ubinds
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index d41161efb1..9d76b655c7 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -15,6 +15,7 @@ open Environ
 open Evd
 open Reductionops
 open Closure
+open Rawterm
 (*i*)
 
 (*s Reduction functions associated to tactics. \label{tacred} *)
@@ -60,20 +61,9 @@ val reduce_to_atomic_ind : env ->  evar_map -> types -> inductive * types
    returns [I] and [t'] or fails with a user error *)
 val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 
-open Rawterm
-(*
-type red_expr =
-  | Red of bool    (* raise Redelimination if true otherwise UserError *)
-  | Hnf
-  | Simpl
-  | Cbv of Closure.RedFlags.reds
-  | Lazy of Closure.RedFlags.reds
-  | Unfold of (int list * evaluable_global_reference) list
-  | Fold of constr list
-  | Pattern of (int list * constr * constr) list
-*)
 type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
+val contextually : constr occurrences -> reduction_function->reduction_function
 val reduction_of_redexp : red_expr -> reduction_function
 
 val declare_red_expr : string -> reduction_function -> unit
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 521a08bc2b..dc163ea210 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -152,7 +152,8 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
 
   (* Conversion *)
   | TacReduce of ('constr,'cst) red_expr_gen * 'id raw_hyp_location list
-  | TacChange of 'constr * 'id raw_hyp_location list
+  | TacChange of
+      'constr occurrences option * 'constr * 'id raw_hyp_location list
 
   (* Equivalence relations *)
   | TacReflexivity
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 75bcb0d6be..52661952ef 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -86,7 +86,7 @@ let h_simplest_right  = h_right NoBindings
 
 (* Conversion *)
 let h_reduce r cl  = abstract_tactic (TacReduce (r,cl)) (reduce r cl)
-let h_change c cl  = abstract_tactic (TacChange (c,cl)) (change c cl)
+let h_change oc c cl  = abstract_tactic (TacChange (oc,c,cl)) (change oc c cl)
 
 (* Equivalence relations *)
 let h_reflexivity    = abstract_tactic TacReflexivity intros_reflexivity
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 797315d642..9bef1f2691 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -90,7 +90,8 @@ val h_simplest_right  : tactic
 
 (* Conversion *)
 val h_reduce          : Tacred.red_expr -> hyp_location list -> tactic
-val h_change          : constr -> hyp_location list -> tactic
+val h_change          : 
+  constr occurrences option -> constr -> hyp_location list -> tactic
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
diff --git a/tactics/refine.ml b/tactics/refine.ml
index d1f380e494..1a360f9bad 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -284,7 +284,7 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	let c = pf_concl gl in
 	let newc = mkNamedLetIn id c1 t1 c in
 	tclTHEN 
-	  (change_in_concl newc) 
+	  (change_in_concl None newc) 
 	  (match sgp with 
 	     | [None] -> introduction id
 	     | [Some th] -> tclTHEN (introduction id) (tcc_aux th)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index fa62c8dd46..fd57bce87f 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -636,7 +636,7 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
 	then
 	  let m = morphism_table_find fleche_constr in
 	  let args = Array.of_list (create_args al a m.profil c1 c2) in  
-	    tclTHEN (change_in_concl new_concl)
+	    tclTHEN (change_in_concl None new_concl)
 	      (tclTHENS (apply (mkApp (m.lem, args)))
 		 ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[unfold_constr (ConstRef fleche_cp)]))
 (*		 ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[tclIDTAC])) *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2140640275..a09bfbd120 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -387,15 +387,16 @@ let glob_unfold ist (l,qid) = (l,glob_evaluable_or_metanum ist qid)
 let glob_flag ist red =
   { red with rConst = List.map (glob_evaluable_or_metanum ist) red.rConst }
 
-let glob_pattern ist (l,c) = (l,glob_constr ist c)
+let glob_constr_occurrence ist (l,c) = (l,glob_constr ist c)
 
 let glob_redexp ist = function
   | Unfold l -> Unfold (List.map (glob_unfold ist) l)
   | Fold l -> Fold (List.map (glob_constr ist) l)
   | Cbv f -> Cbv (glob_flag ist f)
   | Lazy f -> Lazy (glob_flag ist f)
-  | Pattern l -> Pattern (List.map (glob_pattern ist) l)
-  | (Red _ | Simpl | Hnf as r) -> r
+  | Pattern l -> Pattern (List.map (glob_constr_occurrence ist) l)
+  | Simpl o -> Simpl (option_app (glob_constr_occurrence ist) o)
+  | (Red _ | Hnf as r) -> r
   | ExtraRedExpr (s,c) -> ExtraRedExpr (s, glob_constr ist c)
 
 (* Interprets an hypothesis name *)
@@ -544,8 +545,9 @@ let rec glob_atomic lf ist = function
   (* Conversion *)
   | TacReduce (r,cl) ->
       TacReduce (glob_redexp ist r, List.map (glob_hyp_location ist) cl)
-  | TacChange (c,cl) ->
-      TacChange (glob_constr ist c, List.map (glob_hyp_location ist) cl)
+  | TacChange (occl,c,cl) ->
+      TacChange (option_app (glob_constr_occurrence ist) occl,
+        glob_constr ist c, List.map (glob_hyp_location ist) cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> TacReflexivity
@@ -1008,7 +1010,8 @@ let redexp_interp ist = function
   | Cbv f -> Cbv (flag_interp ist f)
   | Lazy f -> Lazy (flag_interp ist f)
   | Pattern l -> Pattern (List.map (pattern_interp ist) l)
-  | (Red _ | Simpl | Hnf as r) -> r
+  | Simpl o -> Simpl (option_app (pattern_interp ist) o)
+  | (Red _ |  Hnf as r) -> r
   | ExtraRedExpr (s,c) -> ExtraRedExpr (s,constr_interp ist c)
 
 let interp_may_eval f ist = function
@@ -1661,8 +1664,9 @@ and interp_atomic ist = function
   (* Conversion *)
   | TacReduce (r,cl) ->
       h_reduce (redexp_interp ist r) (List.map (interp_hyp_location ist) cl)
-  | TacChange (c,cl) ->
-      h_change (constr_interp ist c) (List.map (interp_hyp_location ist) cl)
+  | TacChange (occl,c,cl) ->
+      h_change (option_app (pattern_interp ist) occl)
+        (constr_interp ist c) (List.map (interp_hyp_location ist) cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7a2014ae13..6f79e9fcbb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -142,7 +142,7 @@ type tactic_reduction = env -> evar_map -> constr -> constr
    certain hypothesis *)
 
 let reduct_in_concl redfun gl = 
-  convert_concl (pf_reduce redfun gl (pf_concl gl)) gl
+  convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) gl
 
 let reduct_in_hyp redfun idref gl =
   let inhyp,id = match idref with
@@ -151,12 +151,12 @@ let reduct_in_hyp redfun idref gl =
   let (_,c, ty) = pf_get_hyp gl id in
   let redfun' = under_casts (pf_reduce redfun gl) in
   match c with
-    | None -> convert_hyp (id,None,redfun' ty) gl
+    | None -> convert_hyp_no_check (id,None,redfun' ty) gl
     | Some b ->
 	if inhyp then (* Default for defs: reduce in body *)
-	  convert_hyp (id,Some (redfun' b),ty) gl
+	  convert_hyp_no_check (id,Some (redfun' b),ty) gl
 	else
-	  convert_hyp (id,Some b,redfun' ty) gl
+	  convert_hyp_no_check (id,Some b,redfun' ty) gl
 
 let reduct_option redfun = function
   | Some id -> reduct_in_hyp   redfun id 
@@ -166,34 +166,32 @@ let reduct_option redfun = function
    function has to be applied to the conclusion or
    to the hypotheses. *) 
 
-let in_combinator tac1 tac2 = function 
-  | [] -> tac1 
-  | x  -> (tclMAP tac2 x)
-	
 let redin_combinator redfun = function 
   | [] ->  reduct_in_concl redfun 
   | x  -> (tclMAP (reduct_in_hyp redfun) x)
 
 
 (* Now we introduce different instances of the previous tacticals *)
-let change_hyp_and_check t env sigma c =
-  if is_conv env sigma t c then 
+let change_and_check cv_pb t env sigma c =
+  if is_fconv cv_pb env sigma t c then 
     t
   else 
     errorlabstrm "convert-check-hyp" (str "Not convertible")
 
-let change_concl_and_check t env sigma c =
-  if is_conv_leq env sigma t c then 
-    t
-  else 
-    errorlabstrm "convert-check-concl" (str "Not convertible")
+(* Use cumulutavity 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 occl (change_and_check CONV t) 
 
-let change_in_concl t = reduct_in_concl (change_concl_and_check t)
-let change_in_hyp t   = reduct_in_hyp (change_hyp_and_check t)
+let change_in_concl occl t = reduct_in_concl (change_on_subterm CUMUL t occl) 
+let change_in_hyp occl t   = reduct_in_hyp (change_on_subterm CONV t occl)
 
-let change_option t = function
-  | Some id -> reduct_in_hyp   (change_hyp_and_check t) id
-  | None    -> reduct_in_concl (change_concl_and_check t) 
+let change occl c = function
+  | [] -> change_in_concl occl c
+  | l  -> 
+      if List.tl l <> [] & occl <> None then
+	error "No occurrences expected when changing several hypotheses";
+      tclMAP (change_in_hyp occl c) l
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl red_product
@@ -213,8 +211,6 @@ let unfold_in_hyp   loccname   = reduct_in_hyp   (unfoldn loccname)
 let unfold_option   loccname   = reduct_option   (unfoldn loccname) 
 let pattern_option l = reduct_option (pattern_occs l)
 
-let change c = in_combinator (change_in_concl c) (change_in_hyp c)
-
 (* A function which reduces accordingly to a reduction expression,
    as the command Eval does. *)
 
@@ -259,15 +255,13 @@ let id_of_name_with_default s = function
   | Anonymous -> id_of_string s
   | Name id   -> id
 
-let default_id gl =
-  match kind_of_term (strip_outer_cast (pf_concl gl)) with
-    | Prod (name,c1,c2) ->
-  	(match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl c1)) with
-	   | Sort (Prop _) -> (id_of_name_with_default "H" name)
-	   | Sort (Type _) -> (id_of_name_with_default "X" name)
-	   | _                   -> anomaly "Wrong sort")
-    | LetIn (name,b,_,_) -> id_of_name_using_hdchar (pf_env gl) b name
-    | _ -> raise (RefinerError IntroNeedsProduct)
+let default_id gl = function
+  | (name,None,t) ->
+      (match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl t)) with
+	| Sort (Prop _) -> (id_of_name_with_default "H" name)
+	| Sort (Type _) -> (id_of_name_with_default "X" name)
+	| _                   -> anomaly "Wrong sort")
+  | (name,Some b,_) -> id_of_name_using_hdchar (pf_env gl) b name
 
 (* Non primitive introduction tactics are treated by central_intro
    There is possibly renaming, with possibly names to avoid and 
@@ -278,31 +272,32 @@ type intro_name_flag =
   | IntroBasedOn of identifier * identifier list
   | IntroMustBe of identifier
 
+let find_name decl gl = function
+  | IntroAvoid idl        -> fresh_id idl (default_id gl decl) gl
+  | IntroBasedOn (id,idl) -> fresh_id idl id gl
+  | IntroMustBe id        -> 
+      let id' = fresh_id [] id gl in
+      if id' <> id then error ((string_of_id id)^" is already used");
+      id'
+
+let build_intro_tac id = function
+  | None      -> introduction id
+  | Some dest -> tclTHEN (introduction id) (move_hyp true id dest)
+
 let rec intro_gen name_flag move_flag force_flag gl =
-  try
-    let id =
-      match name_flag with
-        | IntroAvoid idl        -> fresh_id idl (default_id gl) gl
-        | IntroBasedOn (id,idl) -> fresh_id idl id gl
-        | IntroMustBe id        -> 
-	    let id' = fresh_id [] id gl in
-  	    if id' <> id then error ((string_of_id id)^" is already used");
-	    id'
-    in
-    begin match move_flag with
-      | None      -> introduction id gl
-      | Some dest -> tclTHEN (introduction id) (move_hyp true id dest) gl
-    end
-  with RefinerError IntroNeedsProduct as e ->
-    if force_flag then
-      try
-        ((tclTHEN (reduce (Red true) [])
-	    (intro_gen name_flag move_flag force_flag)) gl)
-      with Redelimination ->
-        errorlabstrm "Intro" 
-	  (str "No product even after head-reduction")
-    else
-      raise e
+  match kind_of_term (pf_concl gl) with
+    | Prod (name,t,_) -> 
+	build_intro_tac (find_name (name,None,t) gl name_flag) move_flag gl
+    | LetIn (name,b,t,_) ->
+	build_intro_tac (find_name (name,Some b,t) gl name_flag) move_flag gl
+    | _ -> 
+	if not force_flag then raise (RefinerError IntroNeedsProduct);
+	try
+	  tclTHEN
+	    (reduce (Red true) [])
+	    (intro_gen name_flag move_flag force_flag) gl
+	with Redelimination ->
+	  errorlabstrm "Intro" (str "No product even after head-reduction")
 
 let intro_mustbe_force id = intro_gen (IntroMustBe id) None true
 let intro_using id = intro_gen (IntroBasedOn (id,[])) None false
@@ -446,7 +441,7 @@ let bring_hyps hyps =
     (fun gl ->
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
       let f = mkCast (mkMeta (new_meta()),newcl) in
-      refine (mkApp (f, instance_from_named_context hyps)) gl)
+      refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
 
 (* Resolution with missing arguments *)
 
@@ -479,7 +474,6 @@ let apply_with_bindings (c,lbind) gl =
     let clause = make_clenv_binding_apply wc (-1) (c,thm_ty0) lbind in 
     apply kONT clause gl
 
-
 let apply c = apply_with_bindings (c,NoBindings)
 
 let apply_list = function 
@@ -739,23 +733,23 @@ let exact_check c gl =
   let concl = (pf_concl gl) in
   let ct = pf_type_of gl c in
   if pf_conv_x_leq gl ct concl then  
-    refine c gl 
+    refine_no_check c gl 
   else 
     error "Not an exact proof"
 
-let exact_no_check = refine
+let exact_no_check = refine_no_check
 
 let exact_proof c gl =
   (* on experimente la synthese d'ise dans exact *)
   let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
-  in refine c gl 
+  in refine_no_check c gl 
 
 let (assumption : tactic) = fun gl ->
   let concl =  pf_concl gl in 
   let rec arec = function
     | [] -> error "No such assumption"
     | (id,c,t)::rest -> 
-	if pf_conv_x_leq gl t concl then refine (mkVar id) gl
+	if pf_conv_x_leq gl t concl then refine_no_check (mkVar id) gl
 	else arec rest
   in
   arec (pf_hyps gl)
@@ -770,7 +764,7 @@ let (assumption : tactic) = fun gl ->
  * goal. *)                                                               
 
 let clear ids gl = (* avant seul dyn_clear n'echouait pas en [] *)
-  if ids=[] then tclIDTAC gl else thin ids gl
+  if ids=[] then tclIDTAC gl else with_check (thin ids) gl
 
 let clear_body = thin_body
 
@@ -822,7 +816,7 @@ let constructor_tac boundopt i lbind gl =
   end;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
   let apply_tac = apply_with_bindings (cons,lbind) in
-  (tclTHENLIST [convert_concl redcl; intros; apply_tac]) gl
+  (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl
 
 let one_constructor i = constructor_tac None i
 
@@ -956,7 +950,7 @@ let elimination_in_clause_scheme kONT id elimclause indclause =
       [ (* Try to insert the new hyp at the same place *)
         tclORELSE (intro_replacing id)
           (tclTHEN (clear [id]) (introduction id));
-        refine new_hyp_prf])
+        refine_no_check new_hyp_prf])
 
 let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl = 
   let (wc,kONT)  = startWalk gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 2e35c1761c..29107c32a2 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -93,8 +93,8 @@ val try_intros_until :
 
 (*s Exact tactics. *)
 
-val assumption         : tactic
-val exact_no_check      : constr -> tactic
+val assumption       : tactic
+val exact_no_check   : constr -> tactic
 val exact_check      : constr -> tactic
 val exact_proof      : Topconstr.constr_expr -> tactic
 
@@ -105,10 +105,9 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
 val reduct_option     : tactic_reduction -> hyp_location option -> tactic
 val reduct_in_concl   : tactic_reduction -> tactic
-val change_in_concl   : constr -> tactic
-
-val change_in_hyp     : constr -> hyp_location -> tactic
-val change_option     : constr -> hyp_location option -> tactic
+val change_in_concl   : constr occurrences option -> constr -> tactic
+val change_in_hyp     : constr occurrences option -> constr -> hyp_location ->
+  tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location        -> tactic
 val red_option        : hyp_location option -> tactic
@@ -128,7 +127,8 @@ val unfold_option     :
   (int list * evaluable_global_reference) list -> hyp_location option
     -> tactic
 val reduce            : red_expr -> hyp_location list -> tactic
-val change            : constr -> hyp_location list -> tactic
+val change            :
+  constr occurrences option -> constr -> hyp_location list -> tactic
 
 val unfold_constr     : global_reference -> tactic
 val pattern_option  : (int list * constr) list -> hyp_location option -> tactic
@@ -136,7 +136,6 @@ val pattern_option  : (int list * constr) list -> hyp_location option -> tactic
 (*s Modification of the local context. *)
 
 val clear         : identifier list -> tactic
-
 val clear_body    : identifier list -> tactic
 
 val new_hyp       : int option ->constr -> constr substitution -> tactic