Splitting the uses of the unification function according to the status of

the abs flag in rewrite.

1 files changed, 39 insertions, 12 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index c094415999..12fa4e6c73 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -631,10 +631,11 @@ let poly_inverse sort =
 let eq_env x y = x == y
 
 let unify_eqn l2r flags env (sigma, cstrs) hypinfo by t =
+  assert (not hypinfo.abs);
   if isEvar t then None else 
     try
       let hypinfo = 
-      if hypinfo.abs || eq_env hypinfo.cl.env env then hypinfo
+      if eq_env hypinfo.cl.env env then hypinfo
       else refresh_hypinfo env sigma hypinfo
     in
     let {cl=cl; prf=prf; car=car; rel=rel; c1=c1; c2=c2; c=c; abs=abs} = 
@@ -643,10 +644,6 @@ let unify_eqn l2r flags env (sigma, cstrs) hypinfo by t =
     let evd' = Evd.merge sigma cl.evd in
     let cl = { cl with evd = evd' } in
     let hypinfo, evd', prf, c1, c2, car, rel =
-      if abs then
-	let env' = clenv_unify ~flags:rewrite_unif_flags CONV left t cl in
-	  (hypinfo, env'.evd, prf, c1, c2, car, rel)
-      else
 	let env' = clenv_unify ~flags CONV left t cl in
 	  let env' = Clenvtac.clenv_pose_dependent_evars true env' in
 	  let evd' = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
@@ -681,6 +678,33 @@ let unify_eqn l2r flags env (sigma, cstrs) hypinfo by t =
   | e when Class_tactics.catchable e -> None
   | Reduction.NotConvertible -> None
 
+let unify_abs l2r env (sigma, cstrs) hypinfo t =
+  assert (hypinfo.abs && Option.is_empty hypinfo.c);
+  if isEvar t then None else 
+    try
+    let {cl=cl; prf=prf; car=car; rel=rel; c1=c1; c2=c2; } = 
+      hypinfo in
+    let left = if l2r then c1 else c2 in
+    let evd' = Evd.merge sigma cl.evd in
+    let cl = { cl with evd = evd' } in
+    let env' = clenv_unify ~flags:rewrite_unif_flags CONV left t cl in
+    let evd' = env'.evd in
+    let evars = evd', cstrs in
+    let evd, res =
+      if l2r then evars, (prf, (car, rel, c1, c2))
+      else
+        try
+          let evars, symprf = get_symmetric_proof hypinfo.sort env evars car rel in
+            evars, (mkApp (symprf, [| c1 ; c2 ; prf |]),
+                    (car, rel, c2, c1))
+        with Not_found ->
+          let evars, rel' = poly_inverse hypinfo.sort env evars car rel in
+            evars, (prf, (car, rel', c2, c1))
+    in Some ((), evd, res)
+  with 
+  | e when Class_tactics.catchable e -> None
+  | Reduction.NotConvertible -> None
+
 type rewrite_flags = { under_lambdas : bool; on_morphisms : bool }
 
 let default_flags = { under_lambdas = true; on_morphisms = true; }
@@ -811,7 +835,7 @@ let apply_constraint env avoid car rel prf cstr res =
 
 let eq_env x y = x == y
 
-let apply_rule l2r flags by loccs : (hypinfo * int) pure_strategy =
+let apply_rule unify loccs : ('a * int) pure_strategy =
   let (nowhere_except_in,occs) = convert_occs loccs in
   let is_occ occ =
     if nowhere_except_in 
@@ -821,7 +845,7 @@ let apply_rule l2r flags by loccs : (hypinfo * int) pure_strategy =
     fun (hypinfo, occ) env avoid t ty cstr evars ->
       (* if not (eq_env !hypinfo.cl.env env) then *)
       (* 	hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo; *)
-      let unif = unify_eqn l2r flags env evars hypinfo by t in
+      let unif = unify hypinfo env evars t in
 	match unif with
 	| None -> ((hypinfo, occ), Fail)
 	| Some (hypinfo, evars', (prf, (car, rel, c1, c2))) ->
@@ -843,7 +867,8 @@ let apply_lemma l2r flags (evm,c) by loccs : strategy =
 	decompose_applied_relation env (goalevars evars) evars'
 	  None c
     in
-    let _, res = apply_rule l2r flags by loccs (hypinfo,0) env avoid t ty cstr evars in
+    let unify hypinfo env evars t = unify_eqn l2r flags env evars hypinfo by t in
+    let _, res = apply_rule unify loccs (hypinfo,0) env avoid t ty cstr evars in
       (), res
 
 let e_app_poly env evars f args =
@@ -1368,7 +1393,8 @@ let rewrite_with l2r flags c occs : strategy =
     let gevars = goalevars evars in
     let hypinfo = decompose_applied_relation_expr env gevars c in
     let avoid = get_hypinfo_ids hypinfo @ avoid in
-    let app = apply_rule l2r flags None occs in
+    let unify hypinfo env evars t = unify_eqn l2r flags env evars hypinfo None t in
+    let app = apply_rule unify occs in
     let strat = 
       Strategies.fix (fun aux -> 
 	Strategies.choice app (subterm true default_flags aux))
@@ -1972,12 +1998,13 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 (* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
 
 let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
-  let app = apply_rule l2r rewrite_unif_flags None occs in
+  let abs, hypinfo = get_hyp gl (project gl) (c,l) cl l2r in
+  let unify () env evars t = unify_abs l2r env evars hypinfo t in
+  let app = apply_rule unify occs in
   let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
   let substrat = Strategies.fix recstrat in
-  let abs, hypinfo = get_hyp gl (project gl) (c,l) cl l2r in
   let strat () env avoid t ty cstr evars =
-    let _, res = substrat (hypinfo, 0) env avoid t ty cstr evars in
+    let _, res = substrat ((), 0) env avoid t ty cstr evars in
     (), res
   in
   init_setoid ();