[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

7 files changed, 47 insertions, 35 deletions

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)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 65d20a13a1..88b6ab34ff 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -304,22 +304,21 @@ let id_of_class cl =
           mip.(0).Declarations.mind_typename
     | _ -> assert false
 
-let instance_hook info global imps ?hook cst =
-  Impargs.maybe_declare_manual_implicits false cst imps;
+let instance_hook info global ?hook cst =
   let info = intern_info info in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   declare_instance env sigma (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype =
+let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
   let sigma, entry = DeclareDef.prepare_definition
       ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
-  let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
-  Declare.definition_message name;
-  DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
-  instance_hook info global imps ?hook (GlobRef.ConstRef kn)
+  let ubind = Evd.universe_binders sigma in
+  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kn = DeclareDef.declare_definition ~name ~kind ~scope ~ubind ~impargs entry in
+  instance_hook info global ?hook kn
 
 let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
   let subst = List.fold_left2
@@ -332,7 +331,9 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
   let cst = Declare.declare_constant ~name
       ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
-  instance_hook pri global impargs (GlobRef.ConstRef cst)
+  let cst = (GlobRef.ConstRef cst) in
+  Impargs.maybe_declare_manual_implicits false cst impargs;
+  instance_hook pri global cst
 
 let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype =
   let hook { DeclareDef.Hook.S.scope; dref; _ } =
@@ -351,7 +352,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te
     Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls
   in ()
 
-let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
+let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype =
   (* spiwack: it is hard to reorder the actions to do
      the pretyping after the proof has opened. As a
      consequence, we use the low-level primitives to code
@@ -359,12 +360,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decls.(IsDefinition Instance) in
-  let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in
+  let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
   let info = Lemmas.Info.make ~hook ~kind () in
   (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails!
      This is due to a bug in proof_global :( *)
   let termtype = Evarutil.nf_evar sigma termtype in
-  let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma termtype in
+  let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     match term with
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index dc9c8e2d3c..cb9acda770 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -203,6 +203,8 @@ let context_insection sigma ~poly ctx =
           else Monomorphic_entry Univ.ContextSet.empty
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
+        (* XXX Fixme: Use DeclareDef.prepare_definition *)
+        let entry = DeclareDef.ClosedDef.of_proof_entry entry in
         let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
             ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry
         in
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
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index f72954d8c2..9c5cd6fc2a 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -39,6 +39,13 @@ module Hook : sig
   val call : ?hook:t -> S.t -> unit
 end
 
+module ClosedDef : sig
+  type t
+
+  (* Don't use for non-interactive proofs *)
+  val of_proof_entry : Evd.side_effects Declare.proof_entry -> t
+end
+
 val declare_definition
   :  name:Id.t
   -> scope:locality
@@ -46,7 +53,7 @@ val declare_definition
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> ubind:UnivNames.universe_binders
   -> impargs:Impargs.manual_implicits
-  -> Evd.side_effects Declare.proof_entry
+  -> ClosedDef.t
   -> GlobRef.t
 
 val declare_assumption
@@ -88,15 +95,19 @@ val declare_mutually_recursive
   -> Recthm.t list
   -> Names.GlobRef.t list
 
+(* The common use of the returned evar_map is to obtain the universe
+   binders and context for the hook; we should refactor that soon by
+   merging prepare and declare. *)
 val prepare_definition
   :  ?opaque:bool
   -> ?inline:bool
+  -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
   -> poly:bool
   -> udecl:UState.universe_decl
   -> types:EConstr.t option
   -> body:EConstr.t
   -> Evd.evar_map
-  -> Evd.evar_map * Evd.side_effects Declare.proof_entry
+  -> Evd.evar_map * ClosedDef.t
 
 val prepare_obligation
   :  ?opaque:bool
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 24a52eaca4..e643ffa98d 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -362,28 +362,17 @@ let get_fix_exn, stm_get_fix_exn = Hook.make ()
 
 let declare_definition prg =
   let varsubst = obligation_substitution true prg in
-  let body, typ = subst_prog varsubst prg in
-  let nf =
-    UnivSubst.nf_evars_and_universes_opt_subst
-      (fun x -> None)
-      (UState.subst prg.prg_ctx)
-  in
-  let opaque = prg.prg_opaque in
+  let sigma = Evd.from_ctx prg.prg_ctx in
+  let body, types = subst_prog varsubst prg in
+  let body, types = EConstr.(of_constr body, Some (of_constr types)) in
+  let opaque, poly, udecl = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl in
   let fix_exn = Hook.get get_fix_exn () in
-  let typ = nf typ in
-  let body = nf body in
-  let obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in
-  let uvars =
-    Univ.LSet.union
-      (Vars.universes_of_constr typ)
-      (Vars.universes_of_constr body)
-  in
-  let uctx = UState.restrict prg.prg_ctx uvars in
-  let univs =
-    UState.check_univ_decl ~poly:prg.prg_poly uctx prg.prg_univdecl
-  in
-  let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
+  let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
+  (* XXX: This is doing normalization twice *)
+  let sigma, ce =
+    DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in
   let () = progmap_remove prg in
+  let uctx = Evd.evar_universe_context sigma in
   let ubind = UState.universe_binders uctx in
   let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
   DeclareDef.declare_definition
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e4a625d65c..a1bcf95bf5 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -242,6 +242,7 @@ end = struct
         Declare.Internal.map_entry_body pe
           ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff)
     in
+    let pe = DeclareDef.ClosedDef.of_proof_entry pe in
     DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe
 
   let declare_mutdef ~info ~uctx const =