aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc/ccproof.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-07-19 15:31:29 +0200
committerMaxime Dénès2017-07-19 15:31:29 +0200
commite273ff57ef82e81ab6b6309584a7d496ae4659c1 (patch)
tree19dc62a48763943e7de049ee3aab515503038339 /plugins/cc/ccproof.ml
parent28b3bfd84718e5b29f8e3452fcfe22b19e9910dd (diff)
parent6be0e422de395dbdeebb6c481511eb49945eeca8 (diff)
Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.
Diffstat (limited to 'plugins/cc/ccproof.ml')
-rw-r--r--plugins/cc/ccproof.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 4c9ebcfc4d..a43a167e86 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -9,7 +9,6 @@
(* This file uses the (non-compressed) union-find structure to generate *)
(* proof-trees that will be transformed into proof-terms in cctac.ml4 *)
-open API
open CErrors
open Term
open Ccalgo