From 8ac27a8261f5f3fb5d4bf2a207a144df07477910 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 03:42:57 -0400
Subject: [declare] Make the type of closed entries opaque.

This is a step in forcing all entry creation go thru the preparation
functions. We still need to handle plain `Declare.` calls, but this
will be next step.

We need to leave a backdoor for interactive proofs until we unify
proof preparation happening in `Proof_global` with the one happening
in `DeclareDef`, but we are getting there.

TODO: see how to avoid the normalization problems in DeclareObl
---
 plugins/funind/gen_principle.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 4242da2802..47e56b81aa 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -291,6 +291,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
   *)
   let uctx = Evd.evar_universe_context sigma in
   let hook_data = hook, uctx, [] in
+  let entry = DeclareDef.ClosedDef.of_proof_entry entry in
   let _ : Names.GlobRef.t = DeclareDef.declare_definition
       ~name:new_princ_name ~hook_data
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-- 
cgit v1.2.3