From 37cf90492cb6ed468e696fa052192f1a9fc4b003 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Dec 2017 19:31:47 +0100
Subject: Getting rid of pf_matches in Hipattern.

Funnily enough, the old code is completely bogus. It succeeds in early files
of the prelude just because the heterogeneous equality has not been required.
This raises an exception which is not the same one as if we tried to rewrite
with the identity type first.

The only user, the inversion tactic, was actually only relying on Logic.eq
and was furthermore not even using the convertibility algorithm. We just
perform a syntactic match now.
---
 tactics/hipattern.ml  | 17 -----------------
 tactics/hipattern.mli |  3 ---
 tactics/inv.ml        | 12 +++++++++++-
 3 files changed, 11 insertions(+), 21 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3