From 661940fd55a925a6f17f6025f5d15fc9f5647cf9 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 10 Oct 2016 10:59:22 +0200 Subject: Put all plugins behind an "API". --- plugins/funind/merge.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/funind/merge.ml') diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 763443717..290d0bb91 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -8,6 +8,7 @@ (* Merging of induction principles. *) +open API open Globnames open Tactics open Indfun_common -- cgit v1.2.3