Fixing bug #2146 (broken selection of occurrences in "change").

In trunk the different possible combinations of "at" and "in" with
occurrences are taken into account.
In 8.2 branch, it remains fragile (syntaxes that were accepted remain
accepted and a message warns if the occurrences coming after the
"with" are not taken into account).

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

12 files changed, 94 insertions, 64 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3b27b01714..ef41f938d7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -186,6 +186,34 @@ let map_int_or_var f = function
   | Rawterm.ArgArg x -> Rawterm.ArgArg (f x)
   | Rawterm.ArgVar _ as y -> y
 
+let all_concl_occs_clause = { onhyps=Some[]; concl_occs=all_occurrences_expr }
+
+let has_no_specified_occs cl =
+  (cl.onhyps = None || 
+    List.for_all (fun ((occs,_),_) -> occs = all_occurrences_expr)
+    (Option.get cl.onhyps))
+  && (cl.concl_occs = all_occurrences_expr 
+      || cl.concl_occs = no_occurrences_expr)
+
+let merge_occurrences loc cl = function
+  | None ->
+      if has_no_specified_occs cl then (None, cl)
+      else
+	user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.")
+  | Some (occs,p) ->
+      (Some p,
+      if occs = all_occurrences_expr then cl
+      else if cl = all_concl_occs_clause then { onhyps=Some[]; concl_occs=occs }
+      else match cl.onhyps with
+      | Some [(occs',id),l] when
+	  occs' = all_occurrences_expr && cl.concl_occs = no_occurrences_expr ->
+	  { cl with onhyps=Some[(occs,id),l] }
+      | _ ->
+	  if has_no_specified_occs cl then
+	    user_err_loc (loc,"",str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
+	  else
+	    user_err_loc (loc,"",str "Cannot use clause \"at\" twice."))
+
 (* Auxiliary grammar rules *)
 
 GEXTEND Gram
@@ -242,7 +270,7 @@ GEXTEND Gram
 	   all_occurrences_expr_but (List.map (map_int_or_var abs) (n::nl)) ] ]
   ;
   occs:
-    [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr_but [] ] ]
+    [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr ] ]
   ;
   pattern_occ:
     [ [ c = constr; nl = occs -> (nl,c) ] ]
@@ -374,7 +402,7 @@ GEXTEND Gram
   clause_dft_concl:
     [ [ "in"; cl = in_clause -> cl
       | occs=occs -> {onhyps=Some[]; concl_occs=occs}
-      | -> {onhyps=Some[]; concl_occs=all_occurrences_expr} ] ]
+      | -> all_concl_occs_clause ] ]
   ;
   clause_dft_all:
     [ [ "in"; cl = in_clause -> cl
@@ -673,7 +701,8 @@ GEXTEND Gram
       | r = red_tactic; cl = clause_dft_concl -> TacReduce (r, cl)
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
-	  TacChange (oc,c,cl)
+	  let p,cl = merge_occurrences loc cl oc in
+	  TacChange (p,c,cl)
     ] ]
   ;
 END;;
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 7a189dbe4c..cd56bccb73 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -701,16 +701,13 @@ let pr_cases_pattern_expr = pr_patt ltop
 
 let pr_binders = pr_undelimited_binders (pr ltop)
 
-let pr_with_occurrences_with_trailer pr occs trailer =
+let pr_with_occurrences pr occs =
   match occs with
-    ((false,[]),c) -> pr c ++ trailer
+    ((false,[]),c) -> pr c
   | ((nowhere_except_in,nl),c) ->
       hov 1 (pr c ++ spc() ++ str"at " ++
         (if nowhere_except_in then mt() else str "- ") ++
-        hov 0 (prlist_with_sep spc (pr_or_var int) nl) ++ trailer)
-
-let pr_with_occurrences pr occs =
-  pr_with_occurrences_with_trailer pr occs (mt())
+        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 ()) ++
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index f107d59847..1aa173e249 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -54,8 +54,6 @@ val pr_qualid : qualid -> std_ppcmds
 
 val pr_with_occurrences :
   ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
-val pr_with_occurrences_with_trailer :
-  ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds -> std_ppcmds
 val pr_red_expr :
   ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
     ('a,'b,'c) red_expr_gen -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index a96c5b0487..5f02daf4a0 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -841,13 +841,11 @@ and pr_atom1 = function
   | TacReduce (r,h) ->
       hov 1 (pr_red_expr r ++
              pr_clauses (Some true) pr_ident h)
-  | TacChange (occ,c,h) ->
+  | TacChange (op,c,h) ->
       hov 1 (str "change" ++ brk (1,1) ++
-      (match occ with
+      (match op with
           None -> mt()
-        | Some occlc ->
-	    pr_with_occurrences_with_trailer pr_pat occlc
-	      (spc () ++ str "with ")) ++
+        | Some p -> pr_pat p ++ spc () ++ str "with ") ++
       pr_constr c ++ pr_clauses (Some true) pr_ident h)
 
   (* Equivalence relations *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 83c4a2fdc6..1bd5af5336 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -405,10 +405,10 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacReduce (r,cl) ->
       let l = mlexpr_of_clause cl in
       <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >>
-  | Tacexpr.TacChange (occl,c,cl) ->
+  | Tacexpr.TacChange (p,c,cl) ->
       let l = mlexpr_of_clause cl in
-      let g = mlexpr_of_option mlexpr_of_occ_constr in
-      <:expr< Tacexpr.TacChange $g occl$ $mlexpr_of_constr c$ $l$ >>
+      let g = mlexpr_of_option mlexpr_of_constr in
+      <:expr< Tacexpr.TacChange $g p$ $mlexpr_of_constr c$ $l$ >>
 
   (* Equivalence relations *)
   | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >>
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index d16ad78bac..b56e5184e0 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -205,7 +205,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
 
   (* Conversion *)
   | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause
-  | TacChange of 'pat with_occurrences option * 'constr * 'id gclause
+  | TacChange of 'pat option * 'constr * 'id gclause
 
   (* Equivalence relations *)
   | TacReflexivity
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index ba17ac30cd..756212f0a7 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -111,9 +111,8 @@ let h_simplest_right  = h_right false 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 (Option.map Redexpr.out_with_occurrences oc) c cl)
+let h_change op c cl =
+  abstract_tactic (TacChange (op,c,cl)) (change op c cl)
 
 (* Equivalence relations *)
 let h_reflexivity    = abstract_tactic TacReflexivity intros_reflexivity
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index d649c8b315..36b0830dda 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -108,8 +108,7 @@ val h_simplest_right  : tactic
 (* Conversion *)
 val h_reduce          : Redexpr.red_expr -> Tacticals.clause -> tactic
 val h_change          :
-  Pattern.constr_pattern with_occurrences option -> constr -> 
-    Tacticals.clause -> tactic
+  Pattern.constr_pattern option -> constr -> Tacticals.clause -> tactic
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 85986503ed..0e352110a0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -581,13 +581,15 @@ let intern_constr_pattern ist ltacvars pc =
   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
+let intern_typed_pattern ist p =
+  let dummy_pat = PRel 0 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))
+  (intern_constr_gen true false ist p,dummy_pat)
+
+let intern_typed_pattern_with_occurrences ist (l,p) =
+  (l,intern_typed_pattern ist p)
 
 let intern_red_expr ist = function
   | Unfold l -> Unfold (List.map (intern_unfold ist) l)
@@ -801,9 +803,8 @@ let rec intern_atomic lf ist x =
 	     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,
+  | TacChange (Some p,c,cl) ->
+      TacChange (Some (intern_typed_pattern ist p),intern_constr ist c,
 	clause_app (intern_hyp_location ist) cl)
 
   (* Equivalence relations *)
@@ -1369,7 +1370,7 @@ let interp_open_constr_gen kind ist =
 let interp_open_constr ccl =
   interp_open_constr_gen (OfType ccl)
 
-let interp_typed_pattern ist env sigma c =
+let interp_typed_pattern ist env sigma (c,_) =
   let sigma, c =
     interp_gen (OfType None) ist true false false false env sigma c in
   pattern_of_constr sigma c
@@ -1424,7 +1425,7 @@ let interp_flag ist env red =
 let interp_constr_with_occurrences ist sigma env (occs,c) =
   (interp_occurrences ist occs, interp_constr ist sigma env c)
 
-let interp_typed_pattern_with_occurrences ist env sigma (occs,(c,_)) =
+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)
 
@@ -1664,7 +1665,7 @@ let give_context ctxt = function
 (* Reads a pattern by substituting vars of lfun *)
 let use_types = false
 
-let eval_pattern lfun ist env sigma (c,pat) =
+let eval_pattern lfun ist env sigma (_,pat as c) =
   if use_types then
     snd (interp_typed_pattern ist env sigma c)
   else
@@ -2402,10 +2403,9 @@ and interp_atomic ist gl tac =
 	 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)
+  | TacChange (Some op,c,cl) ->
+      let sign,op = interp_typed_pattern ist env sigma op in
+      h_change (Some op)
         (pf_interp_constr ist (extend_gl_hyps gl sign) c)
         (interp_clause ist gl cl)
 
@@ -2625,8 +2625,11 @@ 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_rawconstr_or_pattern subst (c,p) =
+  (subst_rawconstr subst c,subst_pattern subst p)
+
+let subst_pattern_with_occurrences subst (l,p) =
+  (l,subst_rawconstr_or_pattern subst p)
 
 let subst_redexp subst = function
   | Unfold l -> Unfold (List.map (subst_unfold subst) l)
@@ -2644,8 +2647,8 @@ let subst_raw_may_eval subst = function
   | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)
 
 let subst_match_pattern subst = function
-  | Subterm (b,ido,(c,pc)) -> Subterm (b,ido,(subst_rawconstr subst c,subst_pattern subst pc))
-  | Term (c,pc) -> Term (subst_rawconstr subst c,subst_pattern subst pc)
+  | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_rawconstr_or_pattern subst pc))
+  | Term pc -> Term (subst_rawconstr_or_pattern subst pc)
 
 let rec subst_match_goal_hyps subst = function
   | Hyp (locs,mp) :: tl ->
@@ -2725,8 +2728,8 @@ 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_pattern_with_occurrences subst) occl,
+  | TacChange (op,c,cl) ->
+      TacChange (Option.map (subst_rawconstr_or_pattern subst) op,
         subst_rawconstr subst c, cl)
 
   (* Equivalence relations *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e4ff9bf026..af81c7302e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -229,24 +229,12 @@ let error_illegal_clause () =
 let error_illegal_non_atomic_clause () =
   error "\"at\" clause not supported in presence of a non atomic \"in\" clause."
 
-let error_illegal_non_atomic_effective_clause () =
-  error "Unsupported in presence of a non atomic \"in\" clause."
-
 let error_occurrences_not_unsupported () =
   error "Occurrences not supported for this reduction tactic."
 
-let bind_change_occurrences occs nbcl = function
-  | None ->
-      if nbcl > 1 && occs <> all_occurrences_expr then
-	error_illegal_non_atomic_effective_clause ()
-      else
-	None
-  | Some (occl,c) ->
-      if (nbcl > 1 || occs <> all_occurrences_expr) && occl <> all_occurrences
-      then
-	error_illegal_clause ()
-      else
-	Some (Redexpr.out_with_occurrences (occs,c))
+let bind_change_occurrences occs = function
+  | None -> None
+  | Some c -> Some (Redexpr.out_with_occurrences (occs,c))
 
 let bind_red_expr_occurrences occs nbcl redexp =
   let has_at_clause = function
@@ -327,12 +315,11 @@ let change_option occl t = function
 
 let change chg c cls gl =
   let cls = concrete_clause_of cls gl in
-  let nbcl = List.length cls in
   tclMAP (function
     | OnHyp (id,occs,where) ->
-       change_option (bind_change_occurrences occs nbcl chg) c (Some (id,where))
+       change_option (bind_change_occurrences occs chg) c (Some (id,where))
     | OnConcl occs ->
-       change_option (bind_change_occurrences occs nbcl chg) c None)
+       change_option (bind_change_occurrences occs chg) c None)
     cls gl
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e8662a50d4..f556551b0c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -150,7 +150,7 @@ val unfold_in_hyp     :
 val unfold_option     :
   (occurrences * evaluable_global_reference) list -> goal_location -> tactic
 val change            :
-  (occurrences * constr_pattern) option -> constr -> clause -> tactic
+  constr_pattern option -> constr -> clause -> tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> tactic
 val reduce            : red_expr -> clause -> tactic
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index c72ee875af..5ac6ce82b5 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -10,3 +10,23 @@ Goal forall x, 2 + S x = 1 + S x.
 intro. 
 change (?u + S x) with (S (u + x)). 
 Abort.
+
+(* Check the combination of at, with and in (see bug #2146) *)
+
+Goal 3=3 -> 3=3. intro H.
+change 3 at 2 with (1+2) in |- *.
+change 3 at 2 with (1+2) in H |-.
+change 3 with (1+2) in H at 1 |- * at 1.
+(* Now check that there are no more 3's *)
+change 3 with (1+2) in * || reflexivity.
+Qed.
+
+(* Note: the following is invalid and must fail
+change 3 at 1 with (1+2) at 3.
+change 3 at 1 with (1+2) in *.
+change 3 at 1 with (1+2) in H at 2 |-.
+change 3 at 1 with (1+2) in |- * at 3.
+change 3 at 1 with (1+2) in H |- *.
+change 3 at 1 with (1+2) in H, H|-.
+change 3 in |- * at 1.
+ *)