[ComDefinition] Split program from regular declarations

Proof "preparation" [as in `DeclareDef.prepare_definition`] is fairly
more complicated in the Program case; in particular, it includes
checking the existential variables, and elaborating a list of entries
from the holes.

Indeed, in the `Program` case we cannot use
`DeclareDef.prepare_definition` while keeping a good level of
abstraction, so we should introduce a `prepare_obligation` function.

This PR is in preparation for that.

4 files changed, 49 insertions, 28 deletions

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 28cf5c7d98..4242da2802 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -375,7 +375,6 @@ let register_struct is_rec fixpoint_exprl =
       | None ->
         CErrors.user_err ~hdr:"Function" Pp.(str "Body of Function must be given") in
     ComDefinition.do_definition
-      ~program_mode:false
       ~name:fname.CAst.v
       ~poly:false
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index ba2c1ac115..c1be95fa67 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -79,30 +79,38 @@ let check_definition ~program_mode (ce, evd, _, imps) =
   check_evars_are_solved ~program_mode env evd;
   ce
 
-let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+  let program_mode = false in
   let (ce, evd, udecl, impargs as def) =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  if program_mode then
-    let env = Global.env () in
-    let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
-    assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
-    assert(Univ.ContextSet.is_empty ctx);
-    Obligations.check_evars env evd;
-    let c = EConstr.of_constr c in
-    let typ = match ce.Declare.proof_entry_type with
-      | Some t -> EConstr.of_constr t
-      | None -> Retyping.get_type_of env evd c
-    in
-    let obls, _, c, cty =
-      Obligations.eterm_obligations env name evd 0 c typ
-    in
-    let uctx = Evd.evar_universe_context evd in
-    ignore(Obligations.add_definition
-             ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls)
-  else
-    let ce = check_definition ~program_mode def in
-    let uctx = Evd.evar_universe_context evd in
-    let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-    let kind = Decls.IsDefinition kind in
-    ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind:(Evd.universe_binders evd) ce ~impargs)
+  let ce = check_definition ~program_mode def in
+  let uctx = Evd.evar_universe_context evd in
+  let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+  let kind = Decls.IsDefinition kind in
+  let ubind = Evd.universe_binders evd in
+  let _ : Names.GlobRef.t =
+    DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ce ~impargs
+  in ()
+
+let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+  let program_mode = true in
+  let (ce, evd, udecl, impargs as def) =
+    interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
+  in
+  let env = Global.env () in
+  let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
+  assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
+  assert(Univ.ContextSet.is_empty ctx);
+  Obligations.check_evars env evd;
+  let c = EConstr.of_constr c in
+  let typ = match ce.Declare.proof_entry_type with
+    | Some t -> EConstr.of_constr t
+    | None -> Retyping.get_type_of env evd c
+  in
+  let obls, _, c, cty = Obligations.eterm_obligations env name evd 0 c typ in
+  let uctx = Evd.evar_universe_context evd in
+  let _ : DeclareObl.progress =
+    Obligations.add_definition
+      ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
+  in ()
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 6c6da8952e..7902b0ef09 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -15,8 +15,20 @@ open Constrexpr
 (** {6 Definitions/Let} *)
 
 val do_definition
-  :  program_mode:bool
-  -> ?hook:DeclareDef.Hook.t
+  :  ?hook:DeclareDef.Hook.t
+  -> name:Id.t
+  -> scope:DeclareDef.locality
+  -> poly:bool
+  -> kind:Decls.definition_object_kind
+  -> universe_decl_expr option
+  -> local_binder_expr list
+  -> red_expr option
+  -> constr_expr
+  -> constr_expr option
+  -> unit
+
+val do_definition_program
+  :  ?hook:DeclareDef.Hook.t
   -> name:Id.t
   -> scope:DeclareDef.locality
   -> poly:bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5497bd84ac..4806c6bb9c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -567,7 +567,9 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt
       let env = Global.env () in
       let sigma = Evd.from_env env in
       Some (snd (Hook.get f_interp_redexp env sigma r)) in
-  ComDefinition.do_definition ~program_mode ~name:name.v
+  let do_definition =
+    ComDefinition.(if program_mode then do_definition_program else do_definition) in
+  do_definition ~name:name.v
     ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
 
 (* NB: pstate argument to use combinators easily *)