From 8972a5ed75b7778ad992ef018b163c6ac6e27297 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Dec 2017 19:05:19 +0100
Subject: Getting rid of pf_is_matching in Funind.

---
 plugins/funind/recdef.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b0a76137b7..766adfc63a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -141,7 +141,7 @@ let def_id = Id.of_string "def"
 let p_id = Id.of_string "p"
 let rec_res_id = Id.of_string "rec_res";;
 let lt = function () -> (coq_init_constant "lt")
-let le = function () -> (coq_init_constant "le")
+let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le")
 let ex = function () -> (coq_init_constant "ex")
 let nat = function () -> (coq_init_constant "nat")
 let iter_ref () =  
@@ -857,9 +857,13 @@ let rec prove_le g =
     Proofview.V82.of_tactic (apply (delayed_force le_n));
     begin
       try
-	let matching_fun = 
-	  pf_is_matching g
-	    (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in
+        let matching_fun c = match EConstr.kind sigma c with
+        | App (c, [| x0 ; _ |]) ->
+          EConstr.isVar sigma x0 &&
+          Id.equal (destVar sigma x0) (destVar sigma x) &&
+          is_global sigma (le ()) c
+        | _ -> false
+        in
 	let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
 	in 
 	let y = 
-- 
cgit v1.2.3


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(-)

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


From 59cd53f187939ad32c268cc8ec995d58cee4c297 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 7 Dec 2017 11:10:43 +0100
Subject: Remove up-to-conversion matching functions.

They were not used anymore since the previous patches.
---
 API/API.mli                   |  2 --
 pretyping/constr_matching.ml  | 26 +++++++-------------------
 pretyping/constr_matching.mli | 11 -----------
 proofs/tacmach.ml             |  5 -----
 proofs/tacmach.mli            |  8 --------
 5 files changed, 7 insertions(+), 45 deletions(-)

diff --git a/API/API.mli b/API/API.mli
index 6227f17c65..9a671b43b3 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4964,8 +4964,6 @@ sig
 
   val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
 
-  val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool
-
   val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list
 
   val pr_gls    : Goal.goal Evd.sigma -> Pp.t
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 20ef65c884..478ba73fd5 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -13,7 +13,6 @@ open Util
 open Names
 open Globnames
 open Termops
-open Reductionops
 open Term
 open EConstr
 open Vars
@@ -207,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst =
   in
   constrain sigma n c subst
       
-let matches_core env sigma convert allow_partial_app allow_bound_rels
+let matches_core env sigma allow_partial_app allow_bound_rels
     (binding_vars,pat) c =
   let open EConstr in
   let convref ref c = 
@@ -216,11 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
     | ConstRef c, Const (c',_) -> Constant.equal c c'
     | IndRef i, Ind (i', _) -> Names.eq_ind i i'
     | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
-    | _, _ -> 
-      (if convert then 
-	  let sigma,c' = Evd.fresh_global env sigma ref in
-	    is_conv env sigma (EConstr.of_constr c') c
-       else false)
+    | _, _ -> false
   in
   let rec sorec ctx env subst p t =
     let cT = strip_outer_cast sigma t in
@@ -378,14 +373,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
   in
   sorec [] env (Id.Map.empty, Id.Map.empty) pat c
 
-let matches_core_closed env sigma convert allow_partial_app pat c =
-  let names, subst = matches_core env sigma convert allow_partial_app false pat c in
+let matches_core_closed env sigma allow_partial_app pat c =
+  let names, subst = matches_core env sigma allow_partial_app false pat c in
   (names, Id.Map.map snd subst)
 
-let extended_matches env sigma = matches_core env sigma false true true
+let extended_matches env sigma = matches_core env sigma true true
 
 let matches env sigma pat c =
-  snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c)
+  snd (matches_core_closed env sigma true (Id.Set.empty,pat) c)
 
 let special_meta = (-1)
 
@@ -412,7 +407,7 @@ let matches_head env sigma pat c =
 (* Tells if it is an authorized occurrence and if the instance is closed *)
 let authorized_occ env sigma partial_app closed pat c mk_ctx =
   try
-    let subst = matches_core_closed env sigma false partial_app pat c in
+    let subst = matches_core_closed env sigma partial_app pat c in
     if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
     then (fun next -> next ())
     else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
@@ -552,10 +547,3 @@ let is_matching_appsubterm ?(closed=true) env sigma pat c =
   let pat = (Id.Set.empty,pat) in
   let results = sub_match ~partial_app:true ~closed env sigma pat c in
   not (IStream.is_empty results)
-
-let matches_conv env sigma p c =
-  snd (matches_core_closed env sigma true false (Id.Set.empty,p) c)
-
-let is_matching_conv env sigma pat n =
-  try let _ = matches_conv env sigma pat n in true
-  with PatternMatchingFailure -> false
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 780ccc23d1..60e1c34a15 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -55,12 +55,6 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool
     prefix of it matches against [pat] *)
 val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool
 
-(** [matches_conv env sigma] matches up to conversion in environment
-   [(env,sigma)] when constants in pattern are concerned; it raises
-   [PatternMatchingFailure] if not matchable; bindings are given in
-   increasing order based on the numbers given in the pattern *)
-val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
-
 (** The type of subterm matching results: a substitution + a context
    (whose hole is denoted here with [special_meta]) *)
 type matching_result =
@@ -85,8 +79,3 @@ val match_subterm_gen : env -> Evd.evar_map ->
 (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
    against [pat] taking partial subterms into consideration *)
 val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool
-
-(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
-   up to conversion for constants in patterns *)
-val is_matching_conv :
-  env -> Evd.evar_map -> constr_pattern -> constr -> bool
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a8ec4d8ca3..cab8d7b52a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -102,9 +102,6 @@ let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls
 
-let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p c
-let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p c
-
 (********************************************)
 (* Definition of the most primitive tactics *)
 (********************************************)
@@ -223,8 +220,6 @@ module New = struct
   let pf_hnf_type_of gl t =
     pf_whd_all gl (pf_get_type_of gl t)
 
-  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
-
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d9496d2b4f..e0fb8fbc5d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -12,9 +12,7 @@ open Environ
 open EConstr
 open Proof_type
 open Redexpr
-open Pattern
 open Locus
-open Ltac_pretype
 
 (** Operations for handling terms under a local typing context. *)
 
@@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
-val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
-
-
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
@@ -138,8 +132,6 @@ module New : sig
   val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr
   val pf_compute : 'a Proofview.Goal.t -> constr -> constr
 
-  val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
-
   val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
 
 end
-- 
cgit v1.2.3