Make rewrite use the registered elimination schemes

1 files changed, 18 insertions, 14 deletions

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index aa1316f15e..4c6b7cdcb6 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -128,10 +128,9 @@ let newssrcongrtac arg ist gl =
     x, re_sig si sigma in
   let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
   let ssr_congr lr = EConstr.mkApp (arr, lr) in
+  let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
   (* here the two cases: simple equality or arrow *)
-  let equality, _, eq_args, gl' =
-    let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
-    pf_saturate gl (EConstr.of_constr eq) 3 in
+  let equality, _, eq_args, gl' = pf_saturate gl (EConstr.of_constr eq) 3 in
   tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
   (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist)
   (fun () ->
@@ -336,17 +335,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
   let sigma, p = (* The resulting goal *)
     Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
   let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in
-  let elim, gl =
-    let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
+  let sigma, elim =
     let sort = elimination_sort_of_goal gl in
-    let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
-    if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
-    let elim, _ = destConst elim in
-    let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
-    let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in
-    let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
-    mkConst c1', gl in
-  let elim = EConstr.of_constr elim in
+    match Equality.eq_elimination_ref (dir = L2R) sort with
+    | Some r -> Evd.fresh_global env sigma r
+    | None ->
+      let ((kn, i) as ind, _), unfolded_c_ty = Tacred.reduce_to_quantified_ind env sigma c_ty in
+      let sort = elimination_sort_of_goal gl in
+      let sigma, elim = Evd.fresh_global env sigma (Indrec.lookup_eliminator env ind sort) in
+      if dir = R2L then sigma, elim else
+      let elim, _ = EConstr.destConst sigma elim in
+      let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
+      let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in
+      let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
+      sigma, EConstr.of_constr (mkConst c1')
+  in
   let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
   (* We check the proof is well typed *)
   let sigma, proof_ty =
@@ -491,7 +494,8 @@ let rwprocess_rule dir rule gl =
           | _ ->
             let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
             EConstr.mkApp (pi2, ra), sigma in
-        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then
+        let sigma,trty = Evd.fresh_global env sigma Coqlib.(lib_ref "core.True.type") in
+        if EConstr.eq_constr sigma a.(0) trty then
          let s, sigma = sr sigma 2 in
          loop (converse_dir d) sigma s a.(1) rs 0
         else