Merge PR #6338: Remove up-to-conversion term matching

3 files changed, 11 insertions, 21 deletions

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 8e851375a6..2c8ca19722 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -39,7 +39,6 @@ type testing_function  = Evd.evar_map -> EConstr.constr -> bool
 let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
 let meta2 = mkmeta 2
-let meta3 = mkmeta 3
 
 let op2bool = function Some _ -> true | None -> false
 
@@ -460,22 +459,6 @@ let find_this_eq_data_decompose gl eqn =
       user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in
   (lbeq,u,eq_args)
 
-let match_eq_nf gls eqn (ref, hetero) =
-  let n = if hetero then 4 else 3 in
-  let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in
-  let pat = mkPattern (mkGAppRef ref args) in
-  match Id.Map.bindings (pf_matches gls pat eqn) with
-    | [(m1,t);(m2,x);(m3,y)] ->
-        assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
-	(t,pf_whd_all gls x,pf_whd_all gls y)
-    | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.")
-
-let dest_nf_eq gls eqn =
-  try
-    snd (first_match (match_eq_nf gls eqn) equalities)
-  with PatternMatchingFailure ->
-    user_err Pp.(str "Not an equality.")
-
 (*** Sigma-types *)
 
 let match_sigma env sigma ex =
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 8ff6fe95c6..237ed42d55 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -144,9 +144,6 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool
    [t,u,T] and a boolean telling if equality is on the left side *)
 val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
 
-(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
-val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr)
-
 (** Match a negation *)
 val is_matching_not : Environ.env -> evar_map -> constr -> bool
 val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 46b10bf33e..cb0bbfd0e7 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -334,6 +334,16 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
    If it can discriminate then the goal is proved, if not tries to use it as
    a rewrite rule. It erases the clause which is given as input *)
 
+let dest_nf_eq env sigma t = match EConstr.kind sigma t with
+| App (r, [| t; x; y |]) ->
+  let open Reductionops in
+  let lazy eq = Coqlib.coq_eq_ref in
+  if EConstr.is_global sigma eq r then
+    (t, whd_all env sigma x, whd_all env sigma y)
+  else user_err Pp.(str "Not an equality.")
+| _ ->
+  user_err Pp.(str "Not an equality.")
+
 let projectAndApply as_mode thin avoid id eqname names depids =
   let subst_hyp l2r id =
     tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id)))
@@ -344,7 +354,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
     let sigma = project gl in
     (** We only look at the type of hypothesis "id" *)
     let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
-    let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in
+    let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in
     match (EConstr.kind sigma t1, EConstr.kind sigma t2) with
     | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1
     | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2