- 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

3 files changed, 21 insertions, 21 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 558ca6c218..3d80bd0040 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 a5bd519e26..0160c290f7 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 f4f852d364..13989f03bc 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
 		     )