Use evar clauses instead of meta clauses in Autorewrite hint registration.

This is barely more meaningful but at least we do not rely on an antiquated
API now.

1 files changed, 16 insertions, 22 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 785cc011f4..cc56de066d 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -212,38 +212,32 @@ let inHintRewrite : string * HintDN.t -> Libobject.obj =
     ~cache:cache_hintrewrite
     ~subst:(Some subst_hintrewrite)
 
-open Clenv
-
 type hypinfo = {
-  hyp_ty : types;
-  hyp_left : constr;
-  hyp_right : constr;
+  hyp_ty : EConstr.types;
+  hyp_pat : EConstr.constr;
 }
 
 let decompose_applied_relation env sigma c ctype left2right =
   let find_rel ty =
-    let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in
-    let eqclause = fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)) in
-    let (_, args) = Termops.decompose_app_vect sigma (Clenv.clenv_type eqclause) in
+    (* FIXME: this is nonsense, we generate evars and then we drop the
+       corresponding evarmap. This sometimes works because [Term_dnet] performs
+       evar surgery via [Termops.filtering]. *)
+    let sigma, ty = Clenv.make_evar_clause env sigma ty in
+    let (_, args) = Termops.decompose_app_vect sigma ty.Clenv.cl_concl in
     let len = Array.length args in
     if 2 <= len then
-        let c1 = args.(len - 2) in
-        let c2 = args.(len - 1) in
-        let _ty1, _ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in
-        (* XXX: It looks like mk_clenv_from_env should be fixed instead? *)
-        let open EConstr in
-        let hyp_ty = Unsafe.to_constr ty in
-        let hyp_left = Unsafe.to_constr @@ c1 in
-        let hyp_right = Unsafe.to_constr @@ c2 in
-        Some { hyp_ty; hyp_left; hyp_right; }
+      let c1 = args.(len - 2) in
+      let c2 = args.(len - 1) in
+      Some (if left2right then c1 else c2)
     else None
   in
     match find_rel ctype with
-    | Some c -> Some c
+    | Some c -> Some { hyp_pat = c; hyp_ty = ctype }
     | None ->
         let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
-        match find_rel (it_mkProd_or_LetIn t' ctx) with
-        | Some c -> Some c
+        let ctype = it_mkProd_or_LetIn t' ctx in
+        match find_rel ctype with
+        | Some c -> Some { hyp_pat = c; hyp_ty = ctype }
         | None -> None
 
 let find_applied_relation ?loc env sigma c left2right =
@@ -267,8 +261,8 @@ let add_rew_rules base lrul =
       (fun dn {CAst.loc;v=((c,ctx),b,t)} ->
         let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
         let info = find_applied_relation ?loc env sigma c b in
-        let pat = if b then info.hyp_left else info.hyp_right in
-        let rul = { rew_lemma = c; rew_type = info.hyp_ty;
+        let pat = EConstr.Unsafe.to_constr info.hyp_pat in
+        let rul = { rew_lemma = c; rew_type = EConstr.Unsafe.to_constr info.hyp_ty;
                     rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
                     rew_tac = Option.map intern t}
         in incr counter;