no user defined rule in op comparison

Author: strub

src/ecTheoryReplay.ml

@@ -66,6 +66,10 @@ let ty_compatible env ue (rtyvars, rty) (ntyvars, nty) =
 (* -------------------------------------------------------------------- *)
 let error_body exn b = if not b then raise exn
 
+(* -------------------------------------------------------------------- *)
+let ri_compatible =
+    { EcReduction.full_red with delta_p = (fun _-> `Force); user = false }
+
 (* -------------------------------------------------------------------- *)
 let constr_compatible exn env cs1 cs2 =
   error_body exn (List.length cs1 = List.length cs2);
@@ -122,8 +126,7 @@ let tydecl_compatible env tyd1 tyd2 =
 let expr_compatible exn env s e1 e2 =
   let f1 = EcFol.form_of_expr EcFol.mhr e1 in
   let f2 = EcSubst.subst_form s (EcFol.form_of_expr EcFol.mhr e2) in
-  let ri = { EcReduction.full_red with delta_p = fun _-> `Force; } in
-  error_body exn (EcReduction.is_conv ~ri:ri (EcEnv.LDecl.init env []) f1 f2)
+  error_body exn (EcReduction.is_conv ~ri:ri_compatible (EcEnv.LDecl.init env []) f1 f2)
 
 let get_open_oper exn env p tys =
   let oper = EcEnv.Op.by_path p env in
@@ -135,8 +138,7 @@ let get_open_oper exn env p tys =
 let rec oper_compatible exn env ob1 ob2 =
   match ob1, ob2 with
   | OP_Plain f1, OP_Plain f2 ->
-    let ri = { EcReduction.full_red with delta_p = fun _-> `Force; } in
-    error_body exn (EcReduction.is_conv ~ri:ri (EcEnv.LDecl.init env []) f1 f2)
+    error_body exn (EcReduction.is_conv ~ri:ri_compatible (EcEnv.LDecl.init env []) f1 f2)
   | OP_Plain {f_node = Fop(p,tys)}, _ ->
     let ob1 = get_open_oper exn env p tys  in
     oper_compatible exn env ob1 ob2