[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

1 files changed, 9 insertions, 2 deletions

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 2528dfd38f..84310cba65 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -38,6 +38,13 @@ module Hook = struct
 
 end
 
+module ClosedDef = struct
+
+  type t = Evd.side_effects Declare.proof_entry
+
+  let of_proof_entry x = x
+end
+
 (* Locality stuff *)
 let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   let should_suggest = ce.Declare.proof_entry_opaque &&
@@ -153,14 +160,14 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
 
 (* Preparing proof entries *)
 
-let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
+let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma =
   let env = Global.env () in
   Pretyping.check_evars_are_solved ~program_mode:false env sigma;
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  sigma, definition_entry ?opaque ?inline ?types ~univs body
+  sigma, definition_entry ?fix_exn ?opaque ?inline ?types ~univs body
 
 let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false