hint simplify now extracts rewriting rules from <=>

EasyCrypt · Sep 5, 2023 · 7d59877 · 7d59877
1 parent bcdb9cb
commit 7d59877
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/ecReduction.ml b/src/ecReduction.ml
@@ -1878,6 +1878,7 @@ module User = struct
         let rec doit conds f =
           match sform_of_form (simp f) with
           | SFimp (f1, f2) -> doit (f1 :: conds) f2
+          | SFiff (f1, f2)
           | SFeq  (f1, f2) -> (f1, f2, List.rev conds)
           | _ when ty_equal tbool (EcEnv.ty_hnorm f.f_ty env) ->
             (f, f_true, List.rev conds)