Add pattern term to rewrite rule record

Author: yannl35133

checker/values.ml

@@ -549,6 +549,7 @@ let v_rewrule = v_tuple "rewrite_rule"
     v_array v_name; (* rr_evars *)
     v_map v_evar v_int; (* esubst *)
     v_pattern;    (* pattern *)
+    v_constr;     (* pat_term *)
     v_constr|]    (* replacement *)
 
 let v_puniv = v_opt v_int

kernel/declarations.mli

@@ -346,6 +346,7 @@ type rewrite_rule = {
   rr_evars: Name.t array;
   esubst: int Evar.Map.t;
   pattern: pattern;
+  pat_term: constr;
   replacement: constr;
 }
 

kernel/declareops.ml

@@ -452,15 +452,17 @@ let subst_machine_pattern subst p =
 let subst_rewrite_rules subst ({ rewrules_rules; rewrules_machine } as rules) =
   let body' = List.Smart.map (fun rule ->
       let pattern' = subst_pattern subst rule.pattern in
+      let pat_term' = subst_mps subst rule.pat_term in
       let replacement' = subst_mps subst rule.replacement in
       if
         pattern' == rule.pattern &&
+        pat_term' == rule.pat_term &&
         replacement' == rule.replacement
       then
         rule
       else
         { rr_uctx = rule.rr_uctx; rr_evars = rule.rr_evars; esubst = rule.esubst;
-          pattern=pattern'; replacement=replacement'
+          pattern=pattern'; pat_term=pat_term'; replacement=replacement'
         })
       rewrules_rules
   in

vernac/comRewriteRule.ml

@@ -171,9 +171,10 @@ let interp_rule (pattern, rhs) =
           ++ fnl() ++ Himsg.explain_pretype_error env evd err)
   in
 
+  let pat_term = Vars.subst_univs_level_constr usubst (Environ.j_val j_pat) in
   let replacement = EConstr.to_constr ~abort_on_undefined_evars:false evd (EConstr.Vars.subst_univs_level_constr usubst rhs) in
 
-  let rule = { rr_evars = names.evar_names; rr_uctx = { quals = names.sort_names; univs = names.level_names }; esubst; pattern; replacement } in
+  let rule = { rr_evars = names.evar_names; rr_uctx = { quals = names.sort_names; univs = names.level_names }; esubst; pattern; pat_term; replacement } in
 
   let machine =
     match Rewrite_rules_ops.translate_rewrite_rule env evd rule with