From 9be8376b9c8b1b3fc9b37d1617b26ef54b172ca6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 02:27:54 -0400
Subject: [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.
---
 vernac/comDefinition.ml | 56 ++++++++++++++++++++++++++++---------------------
 1 file changed, 32 insertions(+), 24 deletions(-)

(limited to 'vernac/comDefinition.ml')

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 ()
-- 
cgit v1.2.3