Factorize code of rewrite to make way for a new implementation using the

new proof engine. Correct treatment of the evar set: the tactic
incrementally extends (and potentially refines) the existing sigma and
the internally generated typeclasses constraints are removed from it at
the end as they are always solved. This avoids tricky and costly
evar_map manipulations.


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

5 files changed, 293 insertions, 102 deletions

diff --git a/dev/include b/dev/include
index b72e68ac07..243f9ea5f5 100644
--- a/dev/include
+++ b/dev/include
@@ -27,6 +27,7 @@
 #install_printer  (* goal *)  ppgoal;;
 #install_printer  (* sigma goal *)  ppsigmagoal;;
 #install_printer  (* proof *)  pproof;;
+#install_printer  (* Goal.goal *)  ppgoalgoal;;
 #install_printer  (* pftreestate *)  pppftreestate;;
 #install_printer  (* metaset.t *) ppmetas;;
 #install_printer  (* evar_map *)  ppevm;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 89a6eb5e32..681cb0634e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -114,6 +114,7 @@ let pp_transparent_state s = pp (pr_transparent_state s)
 let ppmetas metas = pp(pr_metaset metas)
 let ppevm evd = pp(pr_evar_map evd)
 let ppclenv clenv = pp(pr_clenv clenv)
+let ppgoalgoal gl = pp(Goal.pr_goal gl)
 (* spiwack: deactivated until a replacement is found
 let ppgoal g = pp(db_pr_goal g)
 let pppftreestate p = pp(print_pftreestate p)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index a48bc2945f..c70eb3ed46 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -22,6 +22,8 @@ type goal = {
 (* spiwack: I don't deal with the tags, yet. It is a worthy discussion
    whether we do want some tags displayed besides the goal or not. *)
 
+let pr_goal {content = e} = Pp.int e
+
 (* access primitive *)
 (* invariant : [e] must exist in [em] *)
 let content evars { content = e } = Evd.find evars e
@@ -130,7 +132,7 @@ module Refinable = struct
     let (e,_) = Term.destEvar ev in
     handle := e::!handle;
     ev
-
+      
   (* [with_type c typ] constrains term [c] to have type [typ].  *)
   let with_type t typ env rdefs _ _ = 
     (* spiwack: this function assumes that no evars can be created during
@@ -171,6 +173,22 @@ module Refinable = struct
     | a::l1 , b::l2 when a=b -> a::(fusion l1 l2)
     | _ , b::l2 -> b::(fusion l1 l2)
 
+  let update_handle handle init_defs post_defs =
+    (* [delta_evars] holds the evars that have been introduced by this
+       refinement (but not immediatly solved) *)
+    (* spiwack: this is the hackish part, don't know how to do any better though. *)
+    let delta_evars = evar_map_filter_undefined
+      (fun ev _ -> not (Evd.mem init_defs ev))
+      post_defs
+    in
+    (* [delta_evars] in the shape of a list of [evar]-s*)
+    let delta_list = List.map fst (Evd.to_list delta_evars) in
+    (* The variables in [myevars] are supposed to be stored
+       in decreasing order. Breaking this invariant might cause
+       many things to go wrong. *)
+    handle := fusion delta_list !handle;
+    delta_evars
+
   (* [constr_of_raw] is a pretyping function. The [check_type] argument
       asks whether the term should have the same type as the conclusion.
       [resolve_classes] is a flag on pretyping functions which, if set to true,
@@ -192,23 +210,15 @@ module Refinable = struct
     let open_constr = 
       Pretyping.Default.understand_tcc_evars ~resolve_classes rdefs env tycon rawc
     in
-    (* [!rdefs] contains the evar_map outputed by  [understand_...] *)
-    let post_defs = !rdefs in
-    (* [delta_evars] holds the evars that have been introduced by this
-       refinement (but not immediatly solved) *)
-    (* spiwack: this is the hackish part, don't know how to do any better though. *)
-    let delta_evars = evar_map_filter_undefined
-      (fun ev _ -> not (Evd.mem init_defs ev))
-      post_defs
-    in
-    (* [delta_evars] in the shape of a list of [evar]-s*)
-    let delta_list = List.map fst (Evd.to_list delta_evars) in
-    (* The variables in [myevars] are supposed to be stored
-       in decreasing order. Breaking this invariant might cause
-       many things to go wrong. *)
-    handle := fusion delta_list !handle ; 
-    open_constr 
-
+      ignore(update_handle handle init_defs !rdefs);
+      open_constr 
+  
+  let constr_of_open_constr handle check_type (evars, c) env rdefs gl info =
+    let delta = update_handle handle !rdefs evars in
+      rdefs := Evd.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs;
+      if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info
+      else c
+ 
 end
 
 (* [refine t] takes a refinable term and use it as a partial proof for current
diff --git a/proofs/goal.mli b/proofs/goal.mli
index fbf7e78e26..69b2693f7e 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -15,6 +15,9 @@ type goal
     sort of communication pipes. But I find it heavy. *)
 val build : Evd.evar -> goal 
 
+(* Debugging help *)
+val pr_goal : goal -> Pp.std_ppcmds
+
 (* [advance sigma g] returns [Some g'] if [g'] is undefined and 
     is the current avatar of [g] (for instance [g] was changed by [clear]
     into [g']). It returns [None] if [g] has been (partially) solved. *)
@@ -75,6 +78,13 @@ module Refinable : sig
   val constr_of_raw : 
     handle -> bool -> bool -> Glob_term.glob_constr -> Term.constr sensitive
 
+  (* [constr_of_open_constr h check_type] transforms an open constr into a 
+     goal-sensitive constr, adding the undefined variables to the set of subgoals.
+     If [check_type] is true, the term is coerced to the conclusion of the goal.
+     It allows to do refinement with already-built terms with holes.
+  *)
+  val constr_of_open_constr : handle -> bool -> Evd.open_constr -> Term.constr sensitive
+
 end
 
 (* [refine t] takes a refinable term and use it as a partial proof for current
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 171d77dd28..ecc8631bff 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -145,6 +145,10 @@ let new_cstr_evar (goal,cstr) env t =
   let cstr', t = Evarutil.new_evar cstr env t in
     (goal, cstr'), t
 
+let new_goal_evar (goal,cstr) env t =
+  let goal', t = Evarutil.new_evar goal env t in
+    (goal', cstr), t
+
 let build_signature evars env m (cstrs : (types * types option) option list)
     (finalcstr : (types * types option) option) =
   let new_evar evars env t =
@@ -316,6 +320,7 @@ let unify_eqn env sigma hypinfo t =
 	      clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl
 	  in
 	  let env' = Clenvtac.clenv_pose_dependent_evars true env' in
+(* 	  let env' = Clenv.clenv_pose_metas_as_evars env' (Evd.undefined_metas env'.evd) in *)
 	  let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in
 	  let env' = { env' with evd = evd' } in
 	  let nf c = Evarutil.nf_evar evd' (Clenv.clenv_nf_meta env' c) in
@@ -516,25 +521,26 @@ let apply_constraint env sigma car rel prf cstr res =
 
 let eq_env x y = x == y
 
+let goalevars evars = fst evars
+let cstrevars evars = snd evars
+
 let apply_rule hypinfo loccs : strategy =
   let (nowhere_except_in,occs) = loccs in
   let is_occ occ =
     if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
   let occ = ref 0 in
     fun env sigma t ty cstr evars ->
-      if not (eq_env !hypinfo.cl.env env) then hypinfo := refresh_hypinfo env sigma !hypinfo;
-      let unif = unify_eqn env sigma hypinfo t in
+      if not (eq_env !hypinfo.cl.env env) then hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo;
+      let unif = unify_eqn env (goalevars evars) hypinfo t in
 	if unif <> None then incr occ;
 	match unif with
 	| Some (env', (prf, (car, rel, c1, c2))) when is_occ !occ ->
 	    begin
 	      if eq_constr t c2 then Some None
 	      else
-		let goalevars = Evd.evar_merge (fst evars)
-		  (Evd.undefined_evars env'.evd)
-		in
 		let res = { rew_car = ty; rew_from = c1;
-			    rew_to = c2; rew_prf = RewPrf (rel, prf); rew_evars = goalevars, snd evars }
+			    rew_to = c2; rew_prf = RewPrf (rel, prf); 
+			    rew_evars = env'.evd, cstrevars evars }
 		in Some (Some (apply_constraint env sigma car rel prf cstr res))
 	    end
 	| _ -> None
@@ -904,14 +910,13 @@ let rewrite_with {it = c; sigma = evm} left2right loccs : strategy =
 let apply_strategy (s : strategy) env sigma concl cstr evars =
   let res =
     s env sigma concl (Typing.type_of env sigma concl)
-      (Option.map snd cstr) !evars
+      (Option.map snd cstr) evars
   in
     match res with
     | None -> None
     | Some None -> Some None
     | Some (Some res) ->
-	evars := res.rew_evars;
-	Some (Some (res.rew_prf, (res.rew_car, res.rew_from, res.rew_to)))
+	Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to))
 
 let split_evars_once sigma evd =
   Evd.fold_undefined (fun ev evi deps ->
@@ -939,7 +944,8 @@ let split_evars sigma evd =
 
 let merge_evars (goal,cstr) = Evd.merge goal cstr
 let solve_constraints env evars =
-  Typeclasses.resolve_typeclasses env ~split:false ~fail:true (merge_evars evars)
+  Typeclasses.resolve_typeclasses env ~split:false ~fail:true
+    (merge_evars evars)
 
 let nf_zeta =
   Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
@@ -950,12 +956,9 @@ let map_rewprf f = function
 
 exception RewriteFailure
 
-let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
-  let concl, is_hyp =
-    match clause with
-	Some id -> pf_get_hyp_typ gl id, Some id
-      | None -> pf_concl gl, None
-  in
+type result = (evar_map * constr option * types) option option
+
+let cl_rewrite_clause_aux ?(abs=None) strat env sigma concl is_hyp : result =
   let cstr =
     let sort = mkProp in
     let impl = Lazy.force impl in
@@ -963,79 +966,218 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
       | None -> (sort, inverse sort impl)
       | Some _ -> (sort, impl)
   in
-  let sigma = project gl in
-  let evars = ref (Evd.create_evar_defs sigma, Evd.empty) in
-  let env = pf_env gl in
+  let evars = (create_evar_defs sigma, Evd.empty) in
   let eq = apply_strategy strat env sigma concl (Some cstr) evars in
     match eq with
-    | Some (Some (p, (car, oldt, newt))) ->
-	(try
-	    let cstrevars = !evars in
-	    let evars = solve_constraints env cstrevars in
-	    let p = map_rewprf 
-	      (fun p -> nf_zeta env evars (Evarutil.nf_evar evars p)) 
-	      p 
-	    in
-	    let newt = Evarutil.nf_evar evars newt in
-	    let abs = Option.map (fun (x, y) ->
-	      Evarutil.nf_evar evars x, Evarutil.nf_evar evars y) abs in
-	    let undef = split_evars (fst cstrevars) evars in
-	    let rewtac =
-	      match is_hyp with
-	      | Some id ->
-		  (match p with
-		  | RewPrf (rel, p) ->
-		      let term =
-			match abs with
-			| None -> p
-			| Some (t, ty) ->
-			    mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
-		      in
-			cut_replacing id newt
-			  (Tacmach.refine_no_check (mkApp (term, [| mkVar id |])))
-		  | RewCast c ->
-		      change_in_hyp None newt (id, InHypTypeOnly))
-		    
-	      | None ->
-		  (match p with
-		  | RewPrf (rel, p) ->
-		      (match abs with
-		      | None ->
-			  let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
-			    tclTHENLAST
-			      (Tacmach.internal_cut_no_check false name newt)
-			      (tclTHEN (Tactics.revert [name]) (Tacmach.refine_no_check p))
-		      | Some (t, ty) ->
-			  Tacmach.refine_no_check
-			    (mkApp (mkLambda (Name (id_of_string "newt"), newt,
-					     mkLambda (Name (id_of_string "lemma"), ty,
-						      mkApp (p, [| mkRel 2 |]))),
-				   [| mkMeta goal_meta; t |])))
-		  | RewCast c -> 
-		      change_in_concl None newt)
-	    in
-	    let evartac =
-	      if not (Evd.is_empty undef) then
-		Refiner.tclEVARS evars
-	      else tclIDTAC
-	    in tclTHENLIST [evartac; rewtac] gl
-	  with
-	  | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
-	  | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
-	      Refiner.tclFAIL_lazy 0
-		(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
-			++ fnl () ++ Himsg.explain_typeclass_error env e)) gl)
+    | Some (Some (p, evars, car, oldt, newt)) ->
+	let evars' = solve_constraints env evars in
+	let p = map_rewprf (fun p -> nf_zeta env evars' (Evarutil.nf_evar evars' p)) p in
+	let newt = Evarutil.nf_evar evars' newt in
+	let abs = Option.map (fun (x, y) ->
+				Evarutil.nf_evar evars' x, Evarutil.nf_evar evars' y) abs in
+	let evars = (* Keep only original evars (potentially instantiated) and goal evars,
+		       the rest has been defined and substituted already. *)
+	  let cstrs = cstrevars evars in
+	  Evd.fold
+	    (fun ev evi acc ->
+	       if not (Evd.mem cstrs ev) then
+		 Evd.add acc ev evi
+	       else acc)
+	    evars' Evd.empty
+	in
+	let res =
+	  match is_hyp with
+	  | Some id ->
+	      (match p with
+	       | RewPrf (rel, p) ->
+		   let term =
+		     match abs with
+		     | None -> p
+		     | Some (t, ty) ->
+			 mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
+		   in
+		     Some (evars, Some (mkApp (term, [| mkVar id |])), newt)
+	       | RewCast c ->
+		   Some (evars, None, newt))
+		
+	  | None ->
+	      (match p with
+	       | RewPrf (rel, p) ->
+		   (match abs with
+		    | None ->
+(* 			let undef, evar = Evarutil.new_evar undef env newt in *)
+(* 			  Some (undef, Some (mkApp (p, [| evar |])), newt) *)
+			Some (evars, Some p, newt)
+		    | Some (t, ty) ->
+			(* 			let undef, evar = Evarutil.new_evar undef env newt in *)
+			(* 			let proof = subst1 t p in *)
+			let proof = mkApp (mkLambda (Name (id_of_string "lemma"), ty, p),
+					   [| t |])
+			in
+			  Some (evars, Some proof, newt))
+	       | RewCast c -> Some (evars, None, newt))
+	in Some res
+    | Some None -> Some None
+    | None -> None
+		   
+let rewrite_refine (evd,c) = 
+  Tacmach.refine c
+
+let cl_rewrite_clause_tac ?abs strat meta clause gl =
+  let evartac evd = Refiner.tclEVARS evd in
+  let treat res =
+    match res with
+    | None -> raise RewriteFailure
     | Some None ->
-	tclFAIL 0 (str"setoid rewrite failed: no progress made") gl
+	tclFAIL 0 (str"setoid rewrite failed: no progress made")
+    | Some (Some (undef, p, newt)) ->
+	let tac = 
+	  match clause, p with
+	  | Some id, Some p ->
+	      cut_replacing id newt (Tacmach.refine p)
+	  | Some id, None -> 
+	      change_in_hyp None newt (id, InHypTypeOnly)
+	  | None, Some p ->
+	      let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
+		tclTHENLAST
+		  (Tacmach.internal_cut_no_check false name newt)
+		  (tclTHEN (Tactics.revert [name]) (Tacmach.refine p))
+	  | None, None -> change_in_concl None newt
+	in tclTHEN (evartac undef) tac
+  in
+  let tac =
+    try
+      let concl, is_hyp =
+	match clause with
+	| Some id -> pf_get_hyp_typ gl id, Some id
+	| None -> pf_concl gl, None
+      in
+      let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) (project gl) concl is_hyp in
+	treat res
+    with
+    | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
+    | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
+	Refiner.tclFAIL_lazy 0
+	  (lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
+		 ++ fnl () ++ Himsg.explain_typeclass_error env e))
+  in tac gl
+
+open Goal
+open Environ
+
+let bind_gl_info f =
+  bind concl (fun c -> bind env (fun v -> bind defs (fun ev -> f c v ev))) 
+
+let fail l s =
+  raise (Refiner.FailError (l, lazy s))
+
+let new_refine c : Goal.subgoals Goal.sensitive =
+  let refable = Goal.Refinable.make
+    (fun handle -> Goal.Refinable.constr_of_open_constr handle true c) 
+  in Goal.bind refable Goal.refine
+
+let assert_replacing id newt tac = 
+  let sens = bind_gl_info 
+    (fun concl env sigma ->
+       let nc' = 
+	 Environ.fold_named_context
+	   (fun _ (n, b, t as decl) nc' ->
+	      if n = id then (n, b, newt) :: nc'
+	      else decl :: nc')
+	   env ~init:[]
+       in
+       let reft = Refinable.make 
+	 (fun h -> 
+	    Goal.bind (Refinable.mkEvar h
+			 (Environ.reset_with_named_context (val_of_named_context nc') env) concl)
+	      (fun ev -> 
+		 Goal.bind (Refinable.mkEvar h env newt)
+		   (fun ev' ->
+		      let inst = 
+			fold_named_context
+			  (fun _ (n, b, t) inst ->
+			     if n = id then ev' :: inst
+			     else if b = None then mkVar n :: inst else inst)
+			  env ~init:[]
+		      in
+		      let (e, args) = destEvar ev in
+			Goal.return (mkEvar (e, Array.of_list inst)))))
+       in Goal.bind reft Goal.refine)
+  in Proofview.tclTHEN (Proofview.tclSENSITIVE sens) 
+       (Proofview.tclFOCUS 2 2 tac)
+
+let cl_rewrite_clause_newtac ?abs strat clause =
+  let treat (res, is_hyp) = 
+    match res with
     | None -> raise RewriteFailure
-
-let cl_rewrite_clause_strat strat clause gl =
+    | Some None ->
+	fail 0 (str"setoid rewrite failed: no progress made")
+    | Some (Some res) ->
+	match is_hyp, res with
+	| Some id, (undef, Some p, newt) ->
+	    assert_replacing id newt (Proofview.tclSENSITIVE (new_refine (undef, p)))
+	| Some id, (undef, None, newt) -> 
+	    Proofview.tclSENSITIVE (Goal.convert_hyp false (id, None, newt))
+	| None, (undef, Some p, newt) ->
+	    let refable = Goal.Refinable.make
+	      (fun handle -> 
+		 Goal.bind env
+		   (fun env -> Goal.bind (Refinable.mkEvar handle env newt)
+		      (fun ev ->
+			 Goal.Refinable.constr_of_open_constr handle true 
+			   (undef, mkApp (p, [| ev |])))))
+	    in
+	      Proofview.tclSENSITIVE (Goal.bind refable Goal.refine)
+	| None, (undef, None, newt) ->
+	    Proofview.tclSENSITIVE (Goal.convert_concl false newt)
+  in
+  let info =
+    bind_gl_info
+      (fun concl env sigma ->
+	 let ty, is_hyp =
+	   match clause with
+	   | Some id -> Environ.named_type id env, Some id
+	   | None -> concl, None
+	 in
+	 let res = 
+	   try cl_rewrite_clause_aux ?abs strat env sigma ty is_hyp 
+	   with
+	   | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
+	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
+	       fail 0 (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
+		       ++ fnl () ++ Himsg.explain_typeclass_error env e)
+	 in return (res, is_hyp))
+  in Proofview.tclGOALBINDU info (fun i -> treat i)
+  
+let cl_rewrite_clause_new_strat ?abs strat clause =
   init_setoid ();
-  let meta = Evarutil.new_meta() in
-  let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in
-    try cl_rewrite_clause_aux strat meta clause gl
+    try cl_rewrite_clause_newtac ?abs strat clause
     with RewriteFailure ->
-      tclFAIL 0 (str"setoid rewrite failed: strategy failed") gl
+      fail 0 (str"setoid rewrite failed: strategy failed")
+
+let cl_rewrite_clause_newtac' l left2right occs clause =
+  Proof_global.run_tactic 
+    (Proofview.tclFOCUS 1 1 
+       (Proofview.tclGOALBINDU
+	  (bind_gl_info (fun concl env sigma ->
+			   let evdref = ref sigma in
+			   let c, _ = Constrintern.interp_constr_evars_impls ~evdref env (fst l) in
+			     return {it = (c, NoBindings) ; sigma = !evdref}))
+	  (fun l' -> cl_rewrite_clause_new_strat (rewrite_with l' left2right occs) clause)))
+
+(* let cl_rewrite_clause_newtac' l left2right occs clause = *)
+(*   Proof_global.run_tactic  *)
+(*     (Proofview.tclFOCUS 1 1  *)
+(*        (cl_rewrite_clause_new_strat (rewrite_with l left2right occs) clause)); *)
+(*   tclIDTAC *)
+
+let cl_rewrite_clause_strat strat clause gl =
+    init_setoid ();
+    let meta = Evarutil.new_meta() in
+    let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in
+     try cl_rewrite_clause_tac strat (mkMeta meta) clause gl
+      with RewriteFailure ->
+        tclFAIL 0 (str"setoid rewrite failed: strategy failed") gl
 
 let cl_rewrite_clause l left2right occs clause gl =
   cl_rewrite_clause_strat (rewrite_with l left2right occs) clause gl
@@ -1154,6 +1296,33 @@ TACTIC EXTEND setoid_rewrite
       [ cl_rewrite_clause c o (occurrences_of occ) (Some id)]
 END
 
+let occurrences_of l = (true,[])
+
+VERNAC COMMAND EXTEND GenRew
+| [ "rew" orient(o) constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] ->
+    [ cl_rewrite_clause_newtac' c o (occurrences_of occ) (Some (snd id)) ]
+| [ "rew" orient(o) constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] ->
+    [ cl_rewrite_clause_newtac' c o (occurrences_of occ) (Some (snd id)) ]
+| [ "rew" orient(o) constr_with_bindings(c) "in" hyp(id) ] ->
+    [ cl_rewrite_clause_newtac' c o all_occurrences (Some (snd id)) ]
+| [ "rew" orient(o) constr_with_bindings(c) "at" occurrences(occ) ] ->
+    [ cl_rewrite_clause_newtac' c o (occurrences_of occ) None ]
+| [ "rew" orient(o) constr_with_bindings(c) ] -> [ cl_rewrite_clause_newtac' c o all_occurrences None ]
+END
+
+(* TACTIC EXTEND GenRew *)
+(* | [ "rew" orient(o) constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] ->  *)
+(*     [ cl_rewrite_clause_newtac' c o (occurrences_of occ) (Some id) ] *)
+(* | [ "rew" orient(o) constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] -> *)
+(*     [ cl_rewrite_clause_newtac' c o (occurrences_of occ) (Some id) ] *)
+(* | [ "rew" orient(o) constr_with_bindings(c) "in" hyp(id) ] ->  *)
+(*     [ cl_rewrite_clause_newtac' c o all_occurrences (Some id) ] *)
+(* | [ "rew" orient(o) constr_with_bindings(c) "at" occurrences(occ) ] ->  *)
+(*     [ cl_rewrite_clause_newtac' c o (occurrences_of occ) None ] *)
+(* | [ "rew" orient(o) constr_with_bindings(c) ] ->  *)
+(*     [ cl_rewrite_clause_newtac' c o all_occurrences None ] *)
+(* END *)
+
 (* let solve_obligation lemma =  *)
 (*   tclTHEN (Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None))) *)
 (*     (eapply_with_bindings (Constrintern.interp_constr Evd.empty (Global.env()) lemma, NoBindings)) *)
@@ -1529,7 +1698,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
       tclWEAK_PROGRESS 
 	(tclTHEN
             (Refiner.tclEVARS hypinfo.cl.evd)
-            (cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl)) gl
+            (cl_rewrite_clause_tac ~abs:hypinfo.abs strat (mkMeta meta) cl)) gl
     with RewriteFailure ->
       let {l2r=l2r; c1=x; c2=y} = hypinfo in
 	raise (Pretype_errors.PretypeError