aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/certificate.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/certificate.ml')
-rw-r--r--plugins/micromega/certificate.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 25579a878..e40a8a273 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -816,7 +816,7 @@ let pivot v (c1,p1) (c2,p2) =
exception FoundProof of prf_rule
-let rec simpl_sys sys =
+let simpl_sys sys =
List.fold_left (fun acc (c,p) ->
match check_sat (c,p) with
| Tauto -> acc