From 661940fd55a925a6f17f6025f5d15fc9f5647cf9 Mon Sep 17 00:00:00 2001
From: Matej Kosik <matej.kosik@inria.fr>
Date: Mon, 10 Oct 2016 10:59:22 +0200
Subject: Put all plugins behind an "API".

---
 plugins/cc/ccalgo.ml        | 1 +
 plugins/cc/ccalgo.mli       | 1 +
 plugins/cc/ccproof.ml       | 1 +
 plugins/cc/ccproof.mli      | 1 +
 plugins/cc/cctac.ml         | 1 +
 plugins/cc/cctac.mli        | 1 +
 plugins/cc/g_congruence.ml4 | 1 +
 7 files changed, 7 insertions(+)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index ba398c385..e8589f2ce 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -10,6 +10,7 @@
 (* Downey,Sethi and Tarjan. *)
 (* Plus some e-matching and constructor handling by P. Corbineau *)
 
+open API
 open CErrors
 open Util
 open Pp
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index c7fa2f56f..871de7253 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Util
 open Term
 open Names
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 642ceba3d..eecb7bc98 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -9,6 +9,7 @@
 (* 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
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index eacbfeac7..4e4d42f86 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Ccalgo
 open Term
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b638f2360..e8b2d7615 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -8,6 +8,7 @@
 
 (* This file is the interface between the c-c algorithm and Coq *)
 
+open API
 open Evd
 open Names
 open Inductiveops
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index b4bb62be8..ef32d2b83 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -7,6 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open EConstr
 
 val proof_tac: Ccproof.proof -> unit Proofview.tactic
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 7e76854b1..43b150c34 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Ltac_plugin
 open Cctac
 open Stdarg
-- 
cgit v1.2.3