[obligations] Functionalize Program state

In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.

Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.

We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.

This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.

Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.

Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.

1 files changed, 13 insertions, 11 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ba08aa2b94..f454c389dc 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -334,7 +334,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
   Impargs.maybe_declare_manual_implicits false cst impargs;
   instance_hook pri global cst
 
-let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype =
+let declare_instance_program pm env sigma ~global ~poly name pri impargs udecl term termtype =
   let hook { Declare.Hook.S.scope; dref; _ } =
     let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in
     let pri = intern_info pri in
@@ -349,9 +349,9 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term
                     Decls.IsDefinition Decls.Instance in
   let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
   let info = Declare.Info.make  ~udecl ~scope ~poly ~kind ~hook () in
-  let _ : Declare.Obls.progress =
-    Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls
-  in ()
+  let pm, _ =
+    Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
+  in pm
 
 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
@@ -493,7 +493,7 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp
   Pretyping.check_evars_are_solved ~program_mode:false env sigma;
   declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
 
-let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
+let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
   let term, termtype, sigma =
     match opt_props with
     | Some props ->
@@ -506,9 +506,10 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri
       term, termtype, sigma in
   let termtype, sigma = do_instance_resolve_TC termtype sigma env in
   if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then
-    declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
+    let () = declare_instance_constant pri global imps ?hook id decl poly sigma term termtype in
+    pm
   else
-    declare_instance_program  env sigma ~global ~poly id pri imps decl term termtype
+    declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype
 
 let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -564,15 +565,16 @@ let new_instance_interactive ?(global=false)
   id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly
     cty k u ctx ctx' pri decl imps subst id opt_props
 
-let new_instance_program ?(global=false)
+let new_instance_program ?(global=false) ~pm
     ~poly instid ctx cl opt_props
     ?(generalize=true) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
     new_instance_common ~program_mode:true ~generalize env instid ctx cl in
-  do_instance_program env env' sigma ?hook ~global ~poly
-    cty k u ctx ctx' pri decl imps subst id opt_props;
-  id
+  let pm =
+    do_instance_program ~pm env env' sigma ?hook ~global ~poly
+      cty k u ctx ctx' pri decl imps subst id opt_props in
+  pm, id
 
 let new_instance ?(global=false)
     ~poly instid ctx cl props