- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)

- Changement au passage de la convention "at -n1 ... -n2" en 
  "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
  pas mélanger des positifs et des négatifs.
- Au passage:
  - simplification de gclause avec fusion de onconcl et concl_occs,
  - généralisation de l'utilisation de la désignation des occurrences par la
    négative aux cas de setoid_rewrite, clrewrite et rewrite at,
  - correction d'un bug de "rewrite in at" qui utilisait le at de la
    conclusion dans les hyps.


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

11 files changed, 63 insertions, 48 deletions

diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml
index b6112e653..813e951cf 100644
--- a/contrib/firstorder/rules.ml
+++ b/contrib/firstorder/rules.ml
@@ -204,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq=
 let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
-  [[],EvalConstRef (destConst (constant "not"));
-   [],EvalConstRef (destConst (constant "iff"))]
+  [all_occurrences,EvalConstRef (destConst (constant "not"));
+   all_occurrences,EvalConstRef (destConst (constant "iff"))]
 
 let normalize_evaluables=
   onAllClauses
@@ -213,4 +213,4 @@ let normalize_evaluables=
 	 None->unfold_in_concl (Lazy.force defined_connectives)
        | Some ((_,id),_)-> 
 	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   (([],id),Tacexpr.InHypTypeOnly))
+	   ((Rawterm.all_occurrences_expr,id),Tacexpr.InHypTypeOnly))
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 558ca6c21..3d80bd004 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -637,7 +637,7 @@ let build_proof
 		    [
 		      h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
 		      thin dyn_infos.rec_hyps;
-		      pattern_option [[-1],t] None;
+		      pattern_option [(false,[1]),t] None;
 		      h_simplest_case t;
 		      (fun g' -> 
 			 let g'_nb_prod = nb_prod (pf_concl g') in 
@@ -1246,7 +1246,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		 in
 		 let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
 		 tclTHENSEQ
-		   [unfold_in_concl [([],Names.EvalConstRef fname)];
+		   [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)];
 		    let do_prove = 
 		      build_proof 
 			interactive_proof
@@ -1347,11 +1347,10 @@ let build_clause eqs =
   {
     Tacexpr.onhyps = 
       Some (List.map 
-	      (fun id -> ([],id),Tacexpr.InHyp)
+	      (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp)
 	      eqs
 	   );
-    Tacexpr.onconcl = false; 
-    Tacexpr.concl_occs = [] 
+    Tacexpr.concl_occs = Rawterm.no_occurrences_expr 
   }
 
 let rec rewrite_eqs_in_eqs eqs = 
@@ -1364,7 +1363,7 @@ let rec rewrite_eqs_in_eqs eqs =
 	       (fun id gl -> 
 		  observe_tac 
 		    (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) 
-		    (tclTRY (Equality.general_rewrite_in true [] id (mkVar eq) false))
+		    (tclTRY (Equality.general_rewrite_in true all_occurrences id (mkVar eq) false))
 		    gl
 	       ) 
 	       eqs
@@ -1386,7 +1385,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 		  (fun g -> 
 		     if is_mes 
 		     then 
-		       unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g 
+		       unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g 
 		     else tclIDTAC g
 		  );
 		  observe_tac "rew_and_finish"
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index a5bd519e2..0160c290f 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -16,6 +16,7 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Tacmach
+open Termops
 open Sign
 open Hiddentac
 
@@ -314,7 +315,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 		 | None -> (id::pre_args,pre_tac)
 		 | Some b ->
 		     (pre_args,
-		      tclTHEN (h_reduce (Rawterm.Unfold([[],EvalVarRef id])) allHyps) pre_tac
+		      tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac
 		     )
 		     
 	     else (pre_args,pre_tac)
@@ -687,7 +688,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  h_generalize (List.map mkVar ids);
 	  thin ids
 	]
-      else unfold_in_concl [([],Names.EvalConstRef (destConst f))]
+      else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))]
     in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in 
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index f4f852d36..13989f03b 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -296,7 +296,7 @@ let  mkCaseEq a  : tactic =
          [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
           (fun g2 ->
 	    change_in_concl None 
-	      (pattern_occs [([-1], a)] (pf_env g2) Evd.empty (pf_concl g2))
+	     (pattern_occs [((false,[1]), a)] (pf_env g2) Evd.empty (pf_concl g2))
 		  g2);
 	  simplest_case a] g);;
 
@@ -323,7 +323,7 @@ let mkDestructEq :
      [h_generalize new_hyps;
       (fun g2 ->
 	change_in_concl None 
-	  (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2);
+	  (pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2);
       simplest_case expr], to_revert
 
 let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
@@ -336,7 +336,7 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		h_intros thin_intros;
 		
 		tclMAP 
-		  (fun eq -> tclTRY (Equality.general_rewrite_in true [] teq eq false)) 
+		  (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences teq eq false)) 
 		  (List.rev eqs);
 		(fun g1 -> 
 		   let ty_teq = pf_type_of g1 (mkVar teq) in 
@@ -397,7 +397,7 @@ let tclUSER tac is_mes l g =
       clear_tac;
       if is_mes 
       then tclTHEN
-             (unfold_in_concl [([], evaluable_of_global_reference
+             (unfold_in_concl [(all_occurrences, evaluable_of_global_reference
                                       (delayed_force ltof_ref))])
              tac
       else tac
@@ -496,7 +496,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
 	   Nameops.out_name k_na,Nameops.out_name def_na
 	 in
 	 tclTHENS
-	   (general_rewrite_bindings false []
+	   (general_rewrite_bindings false all_occurrences
 	      (mkVar eq,
 	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
 				dummy_loc, NamedHyp def_id, mkVar def]) false)
@@ -531,7 +531,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
 	   observe_tac "intros k h' def" (h_intros [k;h';def]);
 	   observe_tac "simple_iter" (simpl_iter onConcl);
 	   observe_tac "unfold functional" 
-	     (unfold_in_concl[([1],evaluable_of_global_reference func)]);
+	     (unfold_in_concl[((true,[1]),evaluable_of_global_reference func)]);
 	   observe_tac "rewriting equations" 
 	     (list_rewrite true eqs);
            observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite  k def bound cond_eqs le_proofs);
@@ -1120,7 +1120,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
   let x = n_x_id ids nargs in
   tclTHENLIST [
     h_intros x;
-    unfold_in_concl [([], evaluable_of_global_reference f)];
+    unfold_in_concl [(all_occurrences, evaluable_of_global_reference f)];
     observe_tac "simplest_case" 
       (simplest_case (mkApp (terminate_constr,
                              Array.of_list (List.map mkVar x))));
@@ -1144,7 +1144,7 @@ let base_leaf_eq func eqs f_id g =
 		  [|mkApp (delayed_force coq_S, [|mkVar p|]);
 		    mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|])));
       simpl_iter onConcl;
-      tclTRY (unfold_in_concl [([1], evaluable_of_global_reference func)]);
+      tclTRY (unfold_in_concl [((true,[1]), evaluable_of_global_reference func)]);
       list_rewrite true eqs;
       apply (delayed_force refl_equal)] g;;
 
@@ -1160,9 +1160,9 @@ let rec introduce_all_values_eq cont_tac functional termine
 	  [forward None (IntroIdentifier heq2)
              (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
            simpl_iter (onHyp heq2);
-           unfold_in_hyp [([1], evaluable_of_global_reference 
+           unfold_in_hyp [((true,[1]), evaluable_of_global_reference 
                              (global_of_constr functional))]
-             (([], heq2), Tacexpr.InHyp);
+             ((all_occurrences_expr, heq2), Tacexpr.InHyp);
            tclTHENS
 	     (fun gls -> 
 		let t_eq = compute_renamed_type gls (mkVar heq2) in 
@@ -1170,7 +1170,7 @@ let rec introduce_all_values_eq cont_tac functional termine
 		  let _,_,t  = destProd t_eq in let def_na,_,_ = destProd t in 
 		  Nameops.out_name def_na
 		in
-		observe_tac "rewrite heq" (general_rewrite_bindings false []
+		observe_tac "rewrite heq" (general_rewrite_bindings false all_occurrences
 		(mkVar heq2,
 		 ExplicitBindings[dummy_loc,NamedHyp def_id,
 				  f]) false) gls)
@@ -1226,7 +1226,7 @@ let rec introduce_all_values_eq cont_tac functional termine
 			       f_S(mkVar pmax');
 			       dummy_loc, NamedHyp def_id, f])
 			 in
-			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false []
+			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences
 								       c_b false))
 			     g
 		     )
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 10fafaefc..6ec0fac42 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -188,7 +188,7 @@ and e_my_find_search db_list local_db hdc concl =
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve (term,cl)) 
 		 (e_trivial_fail_db db_list local_db)
-	   | Unfold_nth c -> unfold_in_concl [[],c]
+	   | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	   | Extern tacast -> Auto.conclPattern concl 
 	       (Option.get p) tacast
        in 
@@ -403,7 +403,7 @@ and my_find_search db_list local_db hdc concl =
 	      tclTHEN 
 		(unify_resolve st (term,cl)) 
 		(trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> unfold_in_concl [[],c]
+	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	  | Extern tacast -> 
 	      conclPattern concl (Option.get p) tacast))
     tacl
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index ac152f906..06b957d9c 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -166,7 +166,7 @@ let make_pbp_atomic_tactic = function
       TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x]))
   | PbpGeneralize (h,args) ->
       let l = List.map make_pbp_pattern args in
-      TacAtom (zz, TacGeneralize [([],make_app (make_var h) l),Anonymous])
+      TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous])
   | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings))
   | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index a2a504fb4..953fb5e79 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1612,7 +1612,7 @@ and natural_fix ig lh g gs narg ltree =
    | _ -> assert false
 and natural_reduce ig lh g gs ge mode la ltree =
   match la with
-    {onhyps=Some[];onconcl=true} -> 
+    {onhyps=Some[]} when la.concl_occs <> no_occurrences_expr -> 
       spv
         [  (natural_lhyp lh ig.ihsg);
           (show_goal2 lh ig g gs ""); 
@@ -1620,7 +1620,7 @@ and natural_reduce ig lh g gs ge mode la ltree =
 		  {ihsg=All_subgoals_hyp;isgintro="simpl"})
              ltree)
         ]
-  | {onhyps=Some[hyp]; onconcl=false} ->
+  | {onhyps=Some[hyp]} when la.concl_occs = no_occurrences_expr ->
       spv
         [  (natural_lhyp lh ig.ihsg);
           (show_goal2 lh ig g gs ""); 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index b041272c1..fa8f05713 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -464,24 +464,31 @@ let (xlate_ident_or_metaid:
     AI (_, x) -> xlate_ident x
   | MetaId(_, x) -> CT_metaid x;;
 
+let nums_of_occs (b,nums) =
+  if b then nums
+  else List.map (function ArgArg x -> ArgArg (-x) | y -> y) nums
+
 let xlate_hyp = function
   | AI (_,id) -> xlate_ident id
   | MetaId _ -> xlate_error "MetaId should occur only in quotations"
 
 let xlate_hyp_location =
  function
-  | (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 ->
+  | (occs, AI (_,id)), InHypTypeOnly ->
+      CT_intype(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
+  | (occs, AI (_,id)), InHypValueOnly ->
+      CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
+  | ((true,[]), AI (_,id)), InHyp ->
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_coerce_ID_to_UNFOLD (xlate_ident id))
-  | (a::l, AI (_,id)), InHyp ->
+  | ((_,a::l as occs), AI (_,id)), InHyp ->
+      let nums = nums_of_occs occs in
+      let a = List.hd nums and l = List.tl nums in
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_unfold_occ (xlate_ident id, 
 			CT_int_ne_list(num_or_var_to_int a, 
                                        nums_or_var_to_int_list_aux l)))
+  | ((false,[]), AI (_,id)), InHyp -> xlate_error "Unused"
   | (_, MetaId _),_ -> 
       xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
 
@@ -494,7 +501,7 @@ let xlate_clause cls =
       | Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in
   CT_clause
     (hyps_info, 
-     if cls.onconcl then 
+     if cls.concl_occs <> no_occurrences_expr then 
        CT_coerce_STAR_to_STAR_OPT CT_star
      else
        CT_coerce_NONE_to_STAR_OPT CT_none)
@@ -667,11 +674,13 @@ let xlate_using = function
   | Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);;
 
 let xlate_one_unfold_block = function
-    ([],qid) -> 
+    ((true,[]),qid) -> 
       CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid)
-  | (n::nums, qid) ->
+  | (((_,_::_) as occs), qid) ->
+      let l = nums_of_occs occs in
       CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid, 
-                    nums_or_var_to_int_ne_list n nums)
+                    nums_or_var_to_int_ne_list (List.hd l) (List.tl l))
+  | ((false,[]), qid) -> xlate_error "Unused"
 ;;
 
 let xlate_with_names = function
@@ -732,7 +741,8 @@ and xlate_red_tactic =
   | CbvVm -> CT_cbvvm
   | Hnf -> CT_hnf
   | Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
-  | Simpl (Some (l,c)) -> 
+  | Simpl (Some (occs,c)) -> 
+      let l = nums_of_occs occs in
       CT_simpl 
 	(CT_coerce_PATTERN_to_PATTERN_OPT
 	   (CT_pattern_occ
@@ -751,9 +761,9 @@ and xlate_red_tactic =
   | Fold formula_list -> 
       CT_fold(CT_formula_list(List.map xlate_formula formula_list))
   | Pattern l ->
-     let pat_list = List.map (fun (nums,c) ->
+     let pat_list = List.map (fun (occs,c) ->
           CT_pattern_occ
-           (CT_int_list (nums_or_var_to_int_list_aux nums),
+           (CT_int_list (nums_or_var_to_int_list_aux (nums_of_occs occs)),
             xlate_formula c)) l in
      (match pat_list with
       | first :: others -> CT_pattern (CT_pattern_ne_list (first, others))
@@ -907,6 +917,7 @@ and xlate_tac =
     | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
     | TacChange (Some(l,c), f, b) -> 
 	(* TODO LATER: combine with other constructions of pattern_occ *)
+	let l = nums_of_occs l in
 	CT_change_local(
 	  CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l), 
 			 xlate_formula c),
@@ -1151,8 +1162,9 @@ and xlate_tac =
     | TacSpecialize (nopt, (c,sl)) ->
      CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl)
     | TacGeneralize [] -> xlate_error ""
-    | TacGeneralize ((([],first),Anonymous) :: cl)
-	when List.for_all (fun ((o,_),na) -> o = [] & na = Anonymous) cl ->
+    | TacGeneralize ((((true,[]),first),Anonymous) :: cl)
+	when List.for_all (fun ((o,_),na) -> o = all_occurrences_expr
+	  & na = Anonymous) cl ->
      CT_generalize
       (CT_formula_ne_list (xlate_formula first, 
                            List.map (fun ((_,c),_) -> xlate_formula c) cl))
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index b96b57d5b..0bb18b3b0 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -133,7 +133,7 @@ let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c
 let generalize_tac t = generalize_time (generalize t)
 let elim t = elim_time (simplest_elim t)
 let exact t = exact_time (Tactics.refine t)
-let unfold s = Tactics.unfold_in_concl [[], Lazy.force s]
+let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s]
  
 let rev_assoc k =
   let rec loop = function
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 66246faf5..92f74d1d9 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -826,9 +826,11 @@ let raw_polynom th op lc gl =
 				     c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS
 		 (tclORELSE
-                   (Setoid_replace.general_s_rewrite true [] c'i_eq_c''i
+                   (Setoid_replace.general_s_rewrite true
+		     Termops.all_occurrences c'i_eq_c''i
                      ~new_goals:[])
-                   (Setoid_replace.general_s_rewrite false [] c'i_eq_c''i
+                   (Setoid_replace.general_s_rewrite false 
+		     Termops.all_occurrences c'i_eq_c''i
                      ~new_goals:[]))
                  [tac]))
 	 else
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index c3caa403e..474b3616a 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -104,7 +104,8 @@ let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
 
 let protect_tac_in map id =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(([],id),InHyp));;
+  Tactics.reduct_option (protect_red map,DEFAULTcast)
+    (Some((all_occurrences_expr,id),InHyp));;
 
 
 TACTIC EXTEND protect_fv