From 223d0ad62896ce3a8831488acec133561cc9244b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 3 May 2020 17:30:13 +0200
Subject: [declare] Add deprecation notices for compat modules.

We will remove this modules and submit the overlays once the
refactoring is done as to avoid churn.
---
 plugins/funind/gen_principle.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 131a6a6e61..07f578d2a8 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -2199,7 +2199,7 @@ let build_scheme fas =
   List.iter2
     (fun (princ_id, _, _) (body, types, univs, opaque) ->
       let (_ : Constant.t) =
-        let opaque = if opaque = Proof_global.Opaque then true else false in
+        let opaque = if opaque = Declare.Opaque then true else false in
         let def_entry = Declare.definition_entry ~univs ~opaque ?types body in
         Declare.declare_constant ~name:princ_id
           ~kind:Decls.(IsProof Theorem)
-- 
cgit v1.2.3