Merge PR #11836: [obligations] Functionalize Program state

Reviewed-by: SkySkimmer
Ack-by: gares

20 files changed, 398 insertions, 317 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 39ca5413cc..2735c5b5eb 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -339,6 +339,10 @@ let understand_state = function
   | "proof" -> "VtModifyProof", false
   | "proof_opt_query" -> "VtReadProofOpt", false
   | "proof_query" -> "VtReadProof", false
+  | "read_program" -> "VtReadProgram", false
+  | "program" -> "VtModifyProgram", false
+  | "declare_program" -> "VtDeclareProgram", false
+  | "program_interactive" -> "VtOpenProofProgram", false
   | s -> fatal ("unsupported state specifier: " ^ s)
 
 let print_body_state state fmt r =
diff --git a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
new file mode 100644
index 0000000000..72ec55a37c
--- /dev/null
+++ b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "11836" ] || [ "$CI_BRANCH" = "obligations+functional" ]; then
+
+    mtac2_CI_REF=obligations+functional
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    paramcoq_CI_REF=obligations+functional
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    equations_CI_REF=obligations+functional
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    metacoq_CI_REF=obligations+functional
+    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+    rewriter_CI_REF=obligations+functional
+    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
+
+fi
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 14d0c04212..743afe4177 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -864,7 +864,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
     Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
   in
   let (_ : _ list) =
-    Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+    Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
+      ~idopt:None
   in
   evd
 
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index ffce2f8c85..45b1713441 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1526,9 +1526,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let lemma =
             fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
-          let (_ : GlobRef.t list) =
-            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
-              ~idopt:None
+          let (_ : _ list) =
+            Declare.Proof.save_regular ~proof:lemma
+              ~opaque:Vernacexpr.Transparent ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
@@ -1599,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                  lemma)
           in
           let (_ : _ list) =
-            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
-              ~idopt:None
+            Declare.Proof.save_regular ~proof:lemma
+              ~opaque:Vernacexpr.Transparent ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 64f62ba1fb..253c95fa67 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -59,7 +59,8 @@ let declare_fun name kind ?univs value =
 
 let defined lemma =
   let (_ : _ list) =
-    Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+    Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
+      ~idopt:None
   in
   ()
 
@@ -1503,7 +1504,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     in
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
     let (_ : _ list) =
-      Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+      Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None
     in
     ()
   in
@@ -1662,7 +1663,11 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   in
   let _ =
     Flags.silently
-      (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
+      (fun () ->
+        let (_ : _ list) =
+          Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None
+        in
+        ())
       ()
   in
   ()
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 81ee6ed5bb..fa176482bf 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,14 +80,14 @@ GRAMMAR EXTEND Gram
 
 open Declare.Obls
 
-let obligation obl tac = with_tac (fun t -> obligation obl t) tac
-let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac
+let obligation ~pm obl tac = with_tac (fun t -> obligation ~pm obl t) tac
+let next_obligation ~pm obl tac = with_tac (fun t -> next_obligation ~pm obl t) tac
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
 
 }
 
-VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof
+VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
 | [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, Some name, Some t) tac }
 | [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
@@ -101,14 +101,14 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_pro
 | [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
 END
 
-VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program
 | [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
     { try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
 | [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
     { try_solve_obligation num None (Some (Tacinterp.interp t)) }
 END
 
-VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program
 | [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
     { try_solve_obligations (Some name) (Some (Tacinterp.interp t)) }
 | [ "Solve" "Obligations" "with" tactic(t) ] ->
@@ -117,14 +117,14 @@ VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF
     { try_solve_obligations None None }
 END
 
-VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF STATE program
 | [ "Solve" "All" "Obligations" "with" tactic(t) ] ->
     { solve_all_obligations (Some (Tacinterp.interp t)) }
 | [ "Solve" "All" "Obligations" ] ->
     { solve_all_obligations None }
 END
 
-VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF STATE program
 | [ "Admit" "Obligations" "of" ident(name) ] -> { admit_obligations (Some name) }
 | [ "Admit" "Obligations" ] -> { admit_obligations None }
 END
@@ -148,14 +148,14 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
     Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
 END
 
-VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program
 | [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) }
 | [ "Obligations" ] -> { show_obligations None }
 END
 
-VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) }
-| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) }
+VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program
+| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
+| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) }
 END
 
 {
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
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 07695b5bef..e1816fb138 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -52,6 +52,7 @@ val new_instance
 
 val new_instance_program
   : ?global:bool (** Not global by default. *)
+  -> pm:Declare.OblState.t
   -> poly:bool
   -> name_decl
   -> local_binder_expr list
@@ -60,7 +61,7 @@ val new_instance_program
   -> ?generalize:bool
   -> ?hook:(GlobRef.t -> unit)
   -> Vernacexpr.hint_info_expr
-  -> Id.t
+  -> Declare.OblState.t * Id.t
 
 val declare_new_instance
   : ?global:bool (** Not global by default. *)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5ee847a17e..37b7106856 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -125,14 +125,14 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
     Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
   in ()
 
-let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let program_mode = true in
   let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
-  let _ : Declare.Obls.progress =
+  let pm, _ =
     let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
     let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
-    Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls
-  in ()
+    Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
+  in pm
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index e3417d0062..d95e64a85f 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -29,6 +29,7 @@ val do_definition
 
 val do_definition_program
   :  ?hook:Declare.Hook.t
+  -> pm:Declare.OblState.t
   -> name:Id.t
   -> scope:Locality.locality
   -> poly:bool
@@ -38,4 +39,4 @@ val do_definition_program
   -> red_expr option
   -> constr_expr
   -> constr_expr option
-  -> unit
+  -> Declare.OblState.t
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 37615fa09c..55901fd604 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -109,7 +109,7 @@ let telescope env sigma l =
 let nf_evar_context sigma ctx =
   List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
 
-let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
+let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
   let open EConstr in
   let open Vars in
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -262,9 +262,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let uctx = Evd.evar_universe_context sigma in
   let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
   let info = Declare.Info.make ~udecl ~poly ~hook () in
-  let _ : Declare.Obls.progress =
-    Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in
-  ()
+  let pm, _ =
+    Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
+  pm
 
 let out_def = function
   | Some def -> def
@@ -275,7 +275,7 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive ~scope ~poly fixkind fixl =
+let do_program_recursive ~pm ~scope ~poly fixkind fixl =
   let cofix = fixkind = Declare.Obls.IsCoFixpoint in
   let (env, rec_sign, udecl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl
@@ -323,15 +323,15 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
   let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
-  Declare.Obls.add_mutual_definitions defs ~info ~uctx ~ntns fixkind
+  Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind
 
-let do_fixpoint ~scope ~poly l =
+let do_fixpoint ~pm ~scope ~poly l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
     | [Some { CAst.v = CWfRec (n,r) }],
       [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
         let recarg = mkIdentC n.CAst.v in
-        build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations
 
     | [Some { CAst.v = CMeasureRec (n, m, r) }],
       [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
@@ -344,7 +344,7 @@ let do_fixpoint ~scope ~poly l =
           user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
         | _, _ -> r
       in
-        build_wellfounded (id, univs, binders, rtype, out_def body_def) poly
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly
           (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
 
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
@@ -352,12 +352,11 @@ let do_fixpoint ~scope ~poly l =
           Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
       let fixkind = Declare.Obls.IsFixpoint annots in
       let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
-      do_program_recursive ~scope ~poly fixkind l
-
+      do_program_recursive ~pm ~scope ~poly fixkind l
     | _, _ ->
-        user_err ~hdr:"do_fixpoint"
-          (str "Well-founded fixpoints not allowed in mutually recursive blocks")
+      CErrors.user_err ~hdr:"do_fixpoint"
+        (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_cofixpoint ~scope ~poly fixl =
+let do_cofixpoint ~pm ~scope ~poly fixl =
   let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
-  do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl
+  do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index e39f62c348..7935cf27fb 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -11,11 +11,16 @@
 open Vernacexpr
 
 (** Special Fixpoint handling when command is activated. *)
-
 val do_fixpoint :
-  (* When [false], assume guarded. *)
-  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
+     pm:Declare.OblState.t
+  -> scope:Locality.locality
+  -> poly:bool
+  -> fixpoint_expr list
+  -> Declare.OblState.t
 
 val do_cofixpoint :
-  (* When [false], assume guarded. *)
-  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
+     pm:Declare.OblState.t
+  -> scope:Locality.locality
+  -> poly:bool
+  -> cofixpoint_expr list
+  -> Declare.OblState.t
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 85359d5b62..df75e121d8 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -33,11 +33,14 @@ module Hook = struct
       }
   end
 
-  type t = (S.t -> unit) CEphemeron.key
+  type 'a g = (S.t -> 'a -> 'a) CEphemeron.key
+  type t = unit g
 
-  let make hook = CEphemeron.create hook
+  let make_g hook = CEphemeron.create hook
+  let make (hook : S.t -> unit) : t = CEphemeron.create (fun x () -> hook x)
 
-  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
+  let call_g ?hook x s = Option.cata (fun hook -> CEphemeron.get hook x s) s hook
+  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x ()) hook
 
 end
 
@@ -653,9 +656,10 @@ let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
   let { CInfo.name; impargs; typ; _ } = cinfo in
   let entry, uctx = prepare_definition ~info ~opaque ~body ~typ sigma in
   let { Info.scope; kind; hook; _ } = info in
-  declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry
+  declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx
 
-let declare_definition = declare_definition_core ~obls:[]
+let declare_definition ~info ~cinfo ~opaque ~body sigma =
+  declare_definition_core ~obls:[] ~info ~cinfo ~opaque ~body sigma |> fst
 
 let prepare_obligation ~name ~types ~body sigma =
   let env = Global.env () in
@@ -683,14 +687,6 @@ let prepare_parameter ~poly ~udecl ~types sigma =
 
 type progress = Remain of int | Dependent | Defined of GlobRef.t
 
-type obligation_resolver =
-     Id.t option
-  -> Int.Set.t
-  -> unit Proofview.tactic option
-  -> progress
-
-type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
-
 module Obls_ = struct
 
 open Constr
@@ -716,10 +712,11 @@ type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
 
 module ProgramDecl = struct
 
-  type t =
+  type 'a t =
     { prg_cinfo : constr CInfo.t
     ; prg_info : Info.t
     ; prg_opaque : bool
+    ; prg_hook : 'a Hook.g option
     ; prg_body : constr
     ; prg_uctx : UState.t
     ; prg_obligations : obligations
@@ -731,7 +728,7 @@ module ProgramDecl = struct
 
   open Obligation
 
-  let make ~info ~cinfo ~opaque ~ntns ~reduce ~deps ~uctx ~body ~fixpoint_kind obls =
+  let make ~info ~cinfo ~opaque ~ntns ~reduce ~deps ~uctx ~body ~fixpoint_kind ?obl_hook obls =
     let obls', body =
       match body with
       | None ->
@@ -761,6 +758,7 @@ module ProgramDecl = struct
     let prg_uctx = UState.make_flexible_nonalgebraic uctx in
     { prg_cinfo = { cinfo with CInfo.typ = reduce cinfo.CInfo.typ }
     ; prg_info = info
+    ; prg_hook = obl_hook
     ; prg_opaque = opaque
     ; prg_body = body
     ; prg_uctx
@@ -923,11 +921,11 @@ let err_not_transp () =
 
 module ProgMap = Id.Map
 
-module StateFunctional = struct
+module State = struct
 
-  type t = ProgramDecl.t CEphemeron.key ProgMap.t
+  type t = t ProgramDecl.t CEphemeron.key ProgMap.t
 
-  let _empty = ProgMap.empty
+  let empty = ProgMap.empty
 
   let pending pm =
     ProgMap.filter
@@ -965,30 +963,12 @@ module StateFunctional = struct
   let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get
 end
 
-module State = struct
-
-  type t = StateFunctional.t
-
-  open StateFunctional
-
-  let prg_ref, prg_tag =
-    Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
-
-  let first_pending () = first_pending !prg_ref
-  let get_unique_open_prog id = get_unique_open_prog !prg_ref id
-  let add id prg = prg_ref := add !prg_ref id prg
-  let fold ~f ~init = fold !prg_ref ~f ~init
-  let all () = all !prg_ref
-  let find id = find !prg_ref id
-
-end
-
 (* In all cases, the use of the map is read-only so we don't expose the ref *)
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
-let check_solved_obligations ~what_for : unit =
-  if not (ProgMap.is_empty !State.prg_ref) then
-    let keys = map_keys !State.prg_ref in
+let check_solved_obligations ~pm ~what_for : unit =
+  if not (ProgMap.is_empty pm) then
+    let keys = map_keys pm in
     let have_string = if Int.equal (List.length keys) 1 then " has " else " have " in
     CErrors.user_err ~hdr:"Program"
       Pp.(
@@ -1084,7 +1064,7 @@ let subst_prog subst prg =
     ( Vars.replace_vars subst' prg.prg_body
     , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
 
-let declare_definition prg =
+let declare_definition ~pm prg =
   let varsubst = obligation_substitution true prg in
   let sigma = Evd.from_ctx prg.prg_uctx in
   let body, types = subst_prog varsubst prg in
@@ -1093,10 +1073,13 @@ let declare_definition prg =
   let name, info, opaque = prg.prg_cinfo.CInfo.name, prg.prg_info, prg.prg_opaque in
   let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
   (* XXX: This is doing normalization twice *)
-  let kn = declare_definition_core ~cinfo ~info ~obls ~body ~opaque sigma in
-  let pm = progmap_remove !State.prg_ref prg in
-  State.prg_ref := pm;
-  kn
+  let kn, uctx = declare_definition_core ~cinfo ~info ~obls ~body ~opaque sigma in
+  (* XXX: We call the obligation hook here, by consistency with the
+     previous imperative behaviour, however I'm not sure this is right *)
+  let pm = Hook.call_g ?hook:prg.prg_hook
+      { Hook.S.uctx; obls; scope = prg.prg_info.Info.scope; dref = kn} pm in
+  let pm = progmap_remove pm prg in
+  pm, kn
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -1117,7 +1100,7 @@ let compute_possible_guardness_evidences n fixbody fixtype =
     let ctx = fst (Term.decompose_prod_n_assum m fixtype) in
     List.map_i (fun i _ -> i) 0 ctx
 
-let declare_mutual_definition l =
+let declare_mutual_definition ~pm l =
   let len = List.length l in
   let first = List.hd l in
   let defobl x =
@@ -1181,34 +1164,33 @@ let declare_mutual_definition l =
   in
   (* Only for the first constant *)
   let dref = List.hd kns in
-  Hook.(
-    call ?hook:first.prg_info.Info.hook {S.uctx = first.prg_uctx; obls; scope; dref});
-  let pm = List.fold_left progmap_remove !State.prg_ref l in
-  State.prg_ref := pm;
-  dref
-
-let update_obls prg obls rem =
+  let s_hook = {Hook.S.uctx = first.prg_uctx; obls; scope; dref} in
+  Hook.call ?hook:first.prg_info.Info.hook s_hook;
+  (* XXX: We call the obligation hook here, by consistency with the
+     previous imperative behaviour, however I'm not sure this is right *)
+  let pm = Hook.call_g ?hook:first.prg_hook s_hook pm in
+  let pm = List.fold_left progmap_remove pm l in
+  pm, dref
+
+let update_obls ~pm prg obls rem =
   let prg_obligations = {obls; remaining = rem} in
   let prg' = {prg with prg_obligations} in
-  let pm = progmap_replace prg' !State.prg_ref in
-  State.prg_ref := pm;
+  let pm = progmap_replace prg' pm in
   obligations_message rem;
-  if rem > 0 then Remain rem
+  if rem > 0 then pm, Remain rem
   else
     match prg'.prg_deps with
     | [] ->
-      let kn = declare_definition prg' in
-      let pm = progmap_remove !State.prg_ref prg' in
-      State.prg_ref := pm;
-      Defined kn
+      let pm, kn = declare_definition ~pm prg' in
+      pm, Defined kn
     | l ->
       let progs =
         List.map (fun x -> CEphemeron.get (ProgMap.find x pm)) prg'.prg_deps
       in
       if List.for_all (fun x -> obligations_solved x) progs then
-        let kn = declare_mutual_definition progs in
-        Defined kn
-      else Dependent
+        let pm, kn = declare_mutual_definition ~pm progs in
+        pm, Defined kn
+      else pm, Dependent
 
 let dependencies obls n =
   let res = ref Int.Set.empty in
@@ -1219,23 +1201,32 @@ let dependencies obls n =
     obls;
   !res
 
-let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto =
+let update_program_decl_on_defined ~pm prg obls num obl ~uctx rem ~auto =
   let obls = Array.copy obls in
   let () = obls.(num) <- obl in
   let prg = {prg with prg_uctx = uctx} in
-  let _progress = update_obls prg obls (pred rem) in
-  let () =
+  let pm, _progress = update_obls ~pm prg obls (pred rem) in
+  let pm =
     if pred rem > 0 then
       let deps = dependencies obls num in
       if not (Int.Set.is_empty deps) then
-        let _progress = auto (Some prg.prg_cinfo.CInfo.name) deps None in
-        ()
-      else ()
-    else ()
+        let pm, _progress = auto ~pm (Some prg.prg_cinfo.CInfo.name) deps None in
+        pm
+      else pm
+    else pm
   in
-  ()
+  pm
+
+type obligation_resolver =
+     pm:State.t
+  -> Id.t option
+  -> Int.Set.t
+  -> unit Proofview.tactic option
+  -> State.t * progress
+
+type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
 
-let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} =
+let obligation_terminator ~pm ~entry ~uctx ~oinfo:{name; num; auto} =
   let env = Global.env () in
   let ty = entry.proof_entry_type in
   let body, uctx = inline_private_constants ~uctx env entry in
@@ -1243,7 +1234,7 @@ let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} =
   Inductiveops.control_only_guard (Global.env ()) sigma
     (EConstr.of_constr body);
   (* Declare the obligation ourselves and drop the hook *)
-  let prg = Option.get (State.find name) in
+  let prg = Option.get (State.find pm name) in
   let {obls; remaining = rem} = prg.prg_obligations in
   let obl = obls.(num) in
   let status =
@@ -1274,16 +1265,17 @@ let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} =
       UState.from_env (Global.env ())
     else uctx
   in
-  update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto;
-  cst
+  let pm =
+    update_program_decl_on_defined ~pm prg obls num obl ~uctx:prg_ctx rem ~auto in
+  pm, cst
 
 (* Similar to the terminator but for the admitted path; this assumes
    the admitted constant was already declared.
 
    FIXME: There is duplication of this code with obligation_terminator
    and Obligations.admit_obligations *)
-let obligation_admitted_terminator {name; num; auto} ctx' dref =
-  let prg = Option.get (State.find name) in
+let obligation_admitted_terminator ~pm {name; num; auto} ctx' dref =
+  let prg = Option.get (State.find pm name) in
   let {obls; remaining = rem} = prg.prg_obligations in
   let obl = obls.(num) in
   let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in
@@ -1308,7 +1300,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
   in
   let obl = {obl with obl_body = Some (DefinedObl (cst, inst))} in
   let () = if transparent then add_hint true prg cst in
-  update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto
+  update_program_decl_on_defined ~pm prg obls num obl ~uctx:ctx' rem ~auto
 
 end
 
@@ -1322,10 +1314,10 @@ module Proof_ending = struct
 
   type t =
     | Regular
-    | End_obligation of obligation_qed_info
+    | End_obligation of Obls_.obligation_qed_info
     | End_derive of { f : Id.t; name : Id.t }
     | End_equations of
-        { hook : Constant.t list -> Evd.evar_map -> unit
+        { hook : pm:Obls_.State.t -> Constant.t list -> Evd.evar_map -> Obls_.State.t
         ; i : Id.t
         ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
         ; sigma : Evd.evar_map
@@ -1951,15 +1943,15 @@ let compute_proof_using_for_admitted proof typ pproofs =
       Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
     | _ -> None
 
-let finish_admitted ~pinfo ~uctx pe =
+let finish_admitted ~pm ~pinfo ~uctx pe =
   let cst = MutualEntry.declare_variable ~pinfo ~uctx pe in
   (* If the constant was an obligation we need to update the program map *)
   match CEphemeron.get pinfo.Proof_info.proof_ending with
   | Proof_ending.End_obligation oinfo ->
-    Obls_.obligation_admitted_terminator oinfo uctx (List.hd cst)
-  | _ -> ()
+    Obls_.obligation_admitted_terminator ~pm oinfo uctx (List.hd cst)
+  | _ -> pm
 
-let save_admitted ~proof =
+let save_admitted ~pm ~proof =
   let udecl = get_universe_decl proof in
   let Proof.{ poly; entry } = Proof.data (get proof) in
   let typ = match Proofview.initial_goals entry with
@@ -1972,7 +1964,7 @@ let save_admitted ~proof =
   let sec_vars = compute_proof_using_for_admitted proof typ pproofs in
   let uctx = get_initial_euctx proof in
   let univs = UState.check_univ_decl ~poly uctx udecl in
-  finish_admitted ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None)
+  finish_admitted ~pm ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None)
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -2013,7 +2005,7 @@ let finish_derived ~f ~name ~entries =
   let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
   [GlobRef.ConstRef ct]
 
-let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
+let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 =
 
   let obls = ref 1 in
   let sigma, recobls =
@@ -2030,8 +2022,8 @@ let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
         sigma, cst) sigma0
       types proof_obj.entries
   in
-  hook recobls sigma;
-  List.map (fun cst -> GlobRef.ConstRef cst) recobls
+  let pm = hook ~pm recobls sigma in
+  pm, List.map (fun cst -> GlobRef.ConstRef cst) recobls
 
 let check_single_entry { entries; uctx } label =
   match entries with
@@ -2039,20 +2031,20 @@ let check_single_entry { entries; uctx } label =
   | _ ->
     CErrors.anomaly ~label Pp.(str "close_proof returned more than one proof term")
 
-let finalize_proof proof_obj proof_info =
+let finalize_proof ~pm proof_obj proof_info =
   let open Proof_ending in
   match CEphemeron.default proof_info.Proof_info.proof_ending Regular with
   | Regular ->
     let entry, uctx = check_single_entry proof_obj "Proof.save" in
-    MutualEntry.declare_mutdef ~entry ~uctx ~pinfo:proof_info
+    pm, MutualEntry.declare_mutdef ~entry ~uctx ~pinfo:proof_info
   | End_obligation oinfo ->
     let entry, uctx = check_single_entry proof_obj "Obligation.save" in
-    Obls_.obligation_terminator ~entry ~uctx ~oinfo
+    Obls_.obligation_terminator ~pm ~entry ~uctx ~oinfo
   | End_derive { f ; name } ->
-    finish_derived ~f ~name ~entries:proof_obj.entries
+    pm, finish_derived ~f ~name ~entries:proof_obj.entries
   | End_equations { hook; i; types; sigma } ->
     let kind = proof_info.Proof_info.info.Info.kind in
-    finish_proved_equations ~kind ~hook i proof_obj types sigma
+    finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma
 
 let err_save_forbidden_in_place_of_qed () =
   CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode")
@@ -2070,16 +2062,24 @@ let process_idopt_for_save ~idopt info =
         err_save_forbidden_in_place_of_qed ()
     in { info with Proof_info.cinfo }
 
-let save ~proof ~opaque ~idopt =
+let save ~pm ~proof ~opaque ~idopt =
   (* Env and sigma are just used for error printing in save_remaining_recthms *)
   let proof_obj = close_proof ~opaque ~keep_body_ucst_separate:false proof in
   let proof_info = process_idopt_for_save ~idopt proof.pinfo in
-  finalize_proof proof_obj proof_info
+  finalize_proof ~pm proof_obj proof_info
+
+let save_regular ~proof ~opaque ~idopt =
+  let open Proof_ending in
+  match CEphemeron.default proof.pinfo.Proof_info.proof_ending Regular with
+  | Regular ->
+    let (_, grs) : Obls_.State.t * _ = save ~pm:Obls_.State.empty ~proof ~opaque ~idopt in
+    grs
+  | _ -> CErrors.anomaly Pp.(str "save_regular: unexpected proof ending")
 
 (***********************************************************************)
 (* Special case to close a lemma without forcing a proof               *)
 (***********************************************************************)
-let save_lemma_admitted_delayed ~proof ~pinfo =
+let save_lemma_admitted_delayed ~pm ~proof ~pinfo =
   let { entries; uctx } = proof in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
@@ -2092,18 +2092,18 @@ let save_lemma_admitted_delayed ~proof ~pinfo =
     | Some typ -> typ in
   let ctx = UState.univ_entry ~poly uctx in
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-  finish_admitted ~uctx ~pinfo (sec_vars, (typ, ctx), None)
+  finish_admitted ~pm ~uctx ~pinfo (sec_vars, (typ, ctx), None)
 
-let save_lemma_proved_delayed ~proof ~pinfo ~idopt =
+let save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt =
   (* vio2vo calls this but with invalid info, we have to workaround
      that to add the name to the info structure *)
   if CList.is_empty pinfo.Proof_info.cinfo then
     let name = get_po_name proof in
     let info = Proof_info.add_first_thm ~pinfo ~name ~typ:EConstr.mkSet ~impargs:[] in
-    finalize_proof proof info
+    finalize_proof ~pm proof info
   else
     let info = process_idopt_for_save ~idopt pinfo in
-    finalize_proof proof info
+    finalize_proof ~pm proof info
 
 end (* Proof module *)
 
@@ -2217,8 +2217,8 @@ let solve_by_tac ?loc name evi t ~poly ~uctx =
     warn_solve_errored ?loc err;
     None
 
-let get_unique_prog prg =
-  match State.get_unique_open_prog prg with
+let get_unique_prog ~pm prg =
+  match State.get_unique_open_prog pm prg with
   | Ok prg -> prg
   | Error [] ->
     Error.no_obligations None
@@ -2241,7 +2241,7 @@ let rec solve_obligation prg num tac =
   let kind = kind_of_obligation (snd obl.obl_status) in
   let evd = Evd.from_ctx (Internal.get_uctx prg) in
   let evd = Evd.update_sigma_env evd (Global.env ()) in
-  let auto n oblset tac = auto_solve_obligations n ~oblset tac in
+  let auto ~pm n oblset tac = auto_solve_obligations ~pm n ~oblset tac in
   let proof_ending =
     let name = Internal.get_name prg in
     Proof_ending.End_obligation {name; num; auto}
@@ -2254,9 +2254,9 @@ let rec solve_obligation prg num tac =
   let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in
   lemma
 
-and obligation (user_num, name, typ) tac =
+and obligation (user_num, name, typ) ~pm tac =
   let num = pred user_num in
-  let prg = get_unique_prog name in
+  let prg = get_unique_prog ~pm name in
   let { obls; remaining } = Internal.get_obligations prg in
   if num >= 0 && num < Array.length obls then
     let obl = obls.(num) in
@@ -2297,7 +2297,7 @@ and solve_obligation_by_tac prg obls i tac =
           else Some prg
       else None
 
-and solve_prg_obligations prg ?oblset tac =
+and solve_prg_obligations ~pm prg ?oblset tac =
   let { obls; remaining } = Internal.get_obligations prg in
   let rem = ref remaining in
   let obls' = Array.copy obls in
@@ -2307,49 +2307,48 @@ and solve_prg_obligations prg ?oblset tac =
     | Some s -> set := s;
       (fun i -> Int.Set.mem i !set)
   in
-  let (), prg =
+  let prg =
     Array.fold_left_i
-      (fun i ((), prg) x ->
+      (fun i prg x ->
         if p i then (
           match solve_obligation_by_tac prg obls' i tac with
-          | None -> (), prg
+          | None -> prg
           | Some prg ->
             let deps = dependencies obls i in
             set := Int.Set.union !set deps;
             decr rem;
-            (), prg)
-        else (), prg)
-      ((), prg) obls'
+            prg)
+        else prg)
+      prg obls'
   in
-  update_obls prg obls' !rem
+  update_obls ~pm prg obls' !rem
 
-and solve_obligations n tac =
-  let prg = get_unique_prog n in
-    solve_prg_obligations prg tac
+and solve_obligations ~pm n tac =
+  let prg = get_unique_prog ~pm n in
+  solve_prg_obligations ~pm prg tac
 
-and solve_all_obligations tac =
-  State.fold ~init:() ~f:(fun k v () ->
-      let _ = solve_prg_obligations v tac in ())
+and solve_all_obligations ~pm tac =
+  State.fold pm ~init:pm ~f:(fun k v pm ->
+      solve_prg_obligations ~pm v tac |> fst)
 
-and try_solve_obligation n prg tac =
-  let prg = get_unique_prog prg in
+and try_solve_obligation ~pm n prg tac =
+  let prg = get_unique_prog ~pm prg in
   let {obls; remaining} = Internal.get_obligations prg in
   let obls' = Array.copy obls in
   match solve_obligation_by_tac prg obls' n tac with
   | Some prg' ->
-    let _r = update_obls prg' obls' (pred remaining) in
-    ()
-  | None -> ()
+    let pm, _ = update_obls ~pm prg' obls' (pred remaining) in
+    pm
+  | None -> pm
 
-and try_solve_obligations n tac =
-  let _ = solve_obligations n tac in
-  ()
+and try_solve_obligations ~pm n tac =
+  solve_obligations ~pm n tac |> fst
 
-and auto_solve_obligations n ?oblset tac : progress =
+and auto_solve_obligations ~pm n ?oblset tac : State.t * progress =
   Flags.if_verbose Feedback.msg_info
     (str "Solving obligations automatically...");
-  let prg = get_unique_prog n in
-  solve_prg_obligations prg ?oblset tac
+  let prg = get_unique_prog ~pm n in
+  solve_prg_obligations ~pm prg ?oblset tac
 
 let show_single_obligation i n obls x =
   let x = subst_deps_obl obls x in
@@ -2379,20 +2378,20 @@ let show_obligations_of_prg ?(msg = true) prg =
          | Some _ -> ())
       obls
 
-let show_obligations ?(msg = true) n =
+let show_obligations ~pm ?(msg = true) n =
   let progs =
     match n with
     | None ->
-      State.all ()
+      State.all pm
     | Some n ->
-      (match State.find n with
+      (match State.find pm n with
        | Some prg -> [prg]
        | None -> Error.no_obligations (Some n))
   in
   List.iter (fun x -> show_obligations_of_prg ~msg x) progs
 
-let show_term n =
-  let prg = get_unique_prog n in
+let show_term ~pm n =
+  let prg = get_unique_prog ~pm n in
   ProgramDecl.show prg
 
 let msg_generating_obl name obls =
@@ -2404,46 +2403,46 @@ let msg_generating_obl name obls =
        info ++ str ", generating " ++ int len ++
        str (String.plural len " obligation"))
 
-let add_definition ~cinfo ~info ?term ~uctx
+let add_definition ~pm ~cinfo ~info ?obl_hook ?term ~uctx
     ?tactic ?(reduce = reduce) ?(opaque = false) obls =
   let prg =
-    ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None obls
+    ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None ?obl_hook obls
   in
   let name = CInfo.get_name cinfo in
   let {obls;_} = Internal.get_obligations prg in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose (msg_generating_obl name) obls;
-    let cst = Obls_.declare_definition prg in
-    Defined cst)
+    let pm, cst = Obls_.declare_definition ~pm prg in
+    pm, Defined cst)
   else
     let () = Flags.if_verbose (msg_generating_obl name) obls in
-    let () = State.add name prg in
-    let res = auto_solve_obligations (Some name) tactic in
+    let pm = State.add pm name prg in
+    let pm, res = auto_solve_obligations ~pm (Some name) tactic in
     match res with
     | Remain rem ->
-      Flags.if_verbose (show_obligations ~msg:false) (Some name);
-      res
-    | _ -> res
+      Flags.if_verbose (show_obligations ~pm ~msg:false) (Some name);
+      pm, res
+    | _ -> pm, res
 
-let add_mutual_definitions l ~info ~uctx
+let add_mutual_definitions l ~pm ~info ?obl_hook ~uctx
     ?tactic ?(reduce = reduce) ?(opaque = false) ~ntns fixkind =
   let deps = List.map (fun (ci,_,_) -> CInfo.get_name ci) l in
   let pm =
     List.fold_left
-      (fun () (cinfo, b, obls) ->
+      (fun pm (cinfo, b, obls) ->
         let prg =
           ProgramDecl.make ~info ~cinfo ~opaque ~body:(Some b) ~uctx ~deps
-            ~fixpoint_kind:(Some fixkind) ~ntns obls ~reduce
+            ~fixpoint_kind:(Some fixkind) ~ntns ~reduce ?obl_hook obls
         in
-        State.add (CInfo.get_name cinfo) prg)
-      () l
+        State.add pm (CInfo.get_name cinfo) prg)
+      pm l
   in
   let pm, _defined =
     List.fold_left
       (fun (pm, finished) x ->
         if finished then (pm, finished)
         else
-          let res = auto_solve_obligations (Some x) tactic in
+          let pm, res = auto_solve_obligations ~pm (Some x) tactic in
           match res with
           | Defined _ ->
             (* If one definition is turned into a constant,
@@ -2454,7 +2453,7 @@ let add_mutual_definitions l ~info ~uctx
   in
   pm
 
-let admit_prog prg =
+let admit_prog ~pm prg =
   let {obls; remaining} = Internal.get_obligations prg in
   let obls = Array.copy obls in
     Array.iteri
@@ -2471,29 +2470,29 @@ let admit_prog prg =
               obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
         | Some _ -> ())
       obls;
-  Obls_.update_obls prg obls 0
+  Obls_.update_obls ~pm prg obls 0
 
 (* get_any_prog *)
-let rec admit_all_obligations () =
-  let prg = State.first_pending () in
+let rec admit_all_obligations ~pm =
+  let prg = State.first_pending pm in
   match prg with
-  | None -> ()
+  | None -> pm
   | Some prg ->
-    let _prog = admit_prog prg in
-    admit_all_obligations ()
+    let pm, _prog = admit_prog ~pm prg in
+    admit_all_obligations ~pm
 
-let admit_obligations n =
+let admit_obligations ~pm n =
   match n with
-  | None -> admit_all_obligations ()
+  | None -> admit_all_obligations ~pm
   | Some _ ->
-    let prg = get_unique_prog n in
-    let _ = admit_prog prg in
-    ()
+    let prg = get_unique_prog ~pm n in
+    let pm, _ = admit_prog ~pm prg in
+    pm
 
-let next_obligation n tac =
+let next_obligation ~pm n tac =
   let prg = match n with
-    | None -> State.first_pending () |> Option.get
-    | Some _ -> get_unique_prog n
+    | None -> State.first_pending pm |> Option.get
+    | Some _ -> get_unique_prog ~pm n
   in
   let {obls; remaining} = Internal.get_obligations prg in
   let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
@@ -2509,7 +2508,6 @@ let check_program_libraries () =
   Coqlib.check_required_library ["Coq";"Program";"Tactics"]
 
 (* aliases *)
-module State = Obls_.State
 let prepare_obligation = prepare_obligation
 let check_solved_obligations = Obls_.check_solved_obligations
 type fixpoint_kind = Obls_.fixpoint_kind =
@@ -2518,3 +2516,5 @@ type nonrec progress = progress =
   | Remain of int | Dependent | Defined of GlobRef.t
 
 end
+
+module OblState = Obls_.State
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 4891e66803..adb5bd026f 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -40,7 +40,9 @@ open Names
    care, as imperative effects may become not supported in the
    future. *)
 module Hook : sig
-  type t
+  type 'a g
+
+  type t = unit g
 
   (** Hooks allow users of the API to perform arbitrary actions at
      proof/definition saving time. For example, to register a constant
@@ -61,6 +63,7 @@ module Hook : sig
       }
   end
 
+  val make_g : (S.t -> 'a -> 'a) -> 'a g
   val make : (S.t -> unit) -> t
   val call : ?hook:t -> S.t -> unit
 end
@@ -147,6 +150,13 @@ val declare_mutually_recursive
 
 (** {2 Declaration of interactive constants }  *)
 
+(** [save] / [save_admitted] can update obligations state, so we need
+   to expose the state here *)
+module OblState : sig
+  type t
+  val empty : t
+end
+
 (** [Declare.Proof.t] Construction of constants using interactive proofs. *)
 module Proof : sig
 
@@ -172,7 +182,7 @@ module Proof : sig
   val start_equations :
        name:Id.t
     -> info:Info.t
-    -> hook:(Constant.t list -> Evd.evar_map -> unit)
+    -> hook:(pm:OblState.t -> Constant.t list -> Evd.evar_map -> OblState.t)
     -> types:(Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
     -> Evd.evar_map
     -> Proofview.telescope
@@ -198,13 +208,21 @@ module Proof : sig
 
   (** Qed a proof  *)
   val save
+    : pm:OblState.t
+    -> proof:t
+    -> opaque:Vernacexpr.opacity_flag
+    -> idopt:Names.lident option
+    -> OblState.t * GlobRef.t list
+
+  (** For proofs known to have [Regular] ending, no need to touch program state. *)
+  val save_regular
     : proof:t
     -> opaque:Vernacexpr.opacity_flag
     -> idopt:Names.lident option
     -> GlobRef.t list
 
   (** Admit a proof *)
-  val save_admitted : proof:t -> unit
+  val save_admitted : pm:OblState.t -> proof:t -> OblState.t
 
   (** [by tac] applies tactic [tac] to the 1st subgoal of the current
       focused proof.
@@ -287,15 +305,17 @@ module Proof : sig
   (** Special cases for delayed proofs, in this case we must provide the
       proof information so the proof won't be forced. *)
   val save_lemma_admitted_delayed :
-    proof:proof_object
+       pm:OblState.t
+    -> proof:proof_object
     -> pinfo:Proof_info.t
-    -> unit
+    -> OblState.t
 
   val save_lemma_proved_delayed
-    : proof:proof_object
+    : pm:OblState.t
+    -> proof:proof_object
     -> pinfo:Proof_info.t
     -> idopt:Names.lident option
-    -> GlobRef.t list
+    -> OblState.t * GlobRef.t list
 
   (** Used by the STM only to store info, should go away *)
   val get_po_name : proof_object -> Id.t
@@ -446,16 +466,9 @@ module Obls : sig
 
 type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
 
-module State : sig
-  (* Internal *)
-  type t
-  val prg_tag : t Summary.Dyn.tag
-end
-
 (** Check obligations are properly solved before closing the
    [what_for] section / module *)
-val check_solved_obligations : what_for:Pp.t -> unit
-
+val check_solved_obligations : pm:OblState.t -> what_for:Pp.t -> unit
 val default_tactic : unit Proofview.tactic ref
 
 (** Resolution status of a program *)
@@ -478,15 +491,17 @@ val prepare_obligation
    will return whether all the obligations were solved; if so, it will
    also register [c] with the kernel. *)
 val add_definition :
-     cinfo:Constr.types CInfo.t
+     pm:OblState.t
+  -> cinfo:Constr.types CInfo.t
   -> info:Info.t
+  -> ?obl_hook: OblState.t Hook.g
   -> ?term:Constr.t
   -> uctx:UState.t
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(Constr.t -> Constr.t)
   -> ?opaque:bool
   -> RetrieveObl.obligation_info
-  -> progress
+  -> OblState.t * progress
 
 (* XXX: unify with MutualEntry *)
 
@@ -494,41 +509,44 @@ val add_definition :
    except it takes a list now. *)
 val add_mutual_definitions :
      (Constr.t CInfo.t * Constr.t * RetrieveObl.obligation_info) list
+  -> pm:OblState.t
   -> info:Info.t
+  -> ?obl_hook: OblState.t Hook.g
   -> uctx:UState.t
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(Constr.t -> Constr.t)
   -> ?opaque:bool
   -> ntns:Vernacexpr.decl_notation list
   -> fixpoint_kind
-  -> unit
+  -> OblState.t
 
 (** Implementation of the [Obligation] command *)
 val obligation :
      int * Names.Id.t option * Constrexpr.constr_expr option
+  -> pm:OblState.t
   -> Genarg.glob_generic_argument option
   -> Proof.t
 
 (** Implementation of the [Next Obligation] command *)
 val next_obligation :
-  Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t
+  pm:OblState.t -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t
 
 (** Implementation of the [Solve Obligation] command *)
 val solve_obligations :
-  Names.Id.t option -> unit Proofview.tactic option -> progress
+  pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t * progress
 
-val solve_all_obligations : unit Proofview.tactic option -> unit
+val solve_all_obligations : pm:OblState.t -> unit Proofview.tactic option -> OblState.t
 
 (** Number of remaining obligations to be solved for this program *)
 val try_solve_obligation :
-  int -> Names.Id.t option -> unit Proofview.tactic option -> unit
+  pm:OblState.t -> int -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t
 
 val try_solve_obligations :
-  Names.Id.t option -> unit Proofview.tactic option -> unit
+  pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t
 
-val show_obligations : ?msg:bool -> Names.Id.t option -> unit
-val show_term : Names.Id.t option -> Pp.t
-val admit_obligations : Names.Id.t option -> unit
+val show_obligations : pm:OblState.t -> ?msg:bool -> Names.Id.t option -> unit
+val show_term : pm:OblState.t -> Names.Id.t option -> Pp.t
+val admit_obligations : pm:OblState.t -> Names.Id.t option -> OblState.t
 
 val check_program_libraries : unit -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6ed8c59f9f..d540e7f93d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -579,7 +579,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let name = vernac_definition_name lid local in
   start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)]
 
-let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
+let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
   let scope = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
@@ -593,13 +593,13 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt
       Some (snd (Hook.get f_interp_redexp env sigma r)) in
   if program_mode then
     let kind = Decls.IsDefinition kind in
-    ComDefinition.do_definition_program ~name:name.v
+    ComDefinition.do_definition_program ~pm ~name:name.v
       ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
   else
     let () =
       ComDefinition.do_definition ~name:name.v
         ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in
-    ()
+    pm
 
 (* NB: pstate argument to use combinators easily *)
 let vernac_start_proof ~atts kind l =
@@ -609,19 +609,20 @@ let vernac_start_proof ~atts kind l =
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
   start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l
 
-let vernac_end_proof ~lemma = let open Vernacexpr in function
+let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
   | Admitted ->
-    Declare.Proof.save_admitted ~proof:lemma
+    Declare.Proof.save_admitted ~pm ~proof:lemma
   | Proved (opaque,idopt) ->
-    let _ : Names.GlobRef.t list = Declare.Proof.save ~proof:lemma ~opaque ~idopt
-    in ()
+    let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque ~idopt
+    in pm
 
-let vernac_exact_proof ~lemma c =
+let vernac_exact_proof ~lemma ~pm c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
   let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in
-  let _ : _ list = Declare.Proof.save ~proof:lemma ~opaque:Opaque ~idopt:None in
-  if not status then Feedback.feedback Feedback.AddedAxiom
+  let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque:Opaque ~idopt:None in
+  if not status then Feedback.feedback Feedback.AddedAxiom;
+  pm
 
 let vernac_assumption ~atts discharge kind l nl =
   let open DefAttributes in
@@ -837,14 +838,15 @@ let vernac_fixpoint_interactive ~atts discharge l =
     CErrors.user_err Pp.(str"Program Fixpoint requires a body");
   ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l
 
-let vernac_fixpoint ~atts discharge l =
+let vernac_fixpoint ~atts ~pm discharge l =
   let open DefAttributes in
   let scope = vernac_fixpoint_common ~atts discharge l in
   if atts.program then
     (* XXX: Switch to the attribute system and match on ~atts *)
-    ComProgramFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l
+    ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic l
   else
-    ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l
+    let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l in
+    pm
 
 let vernac_cofixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
@@ -858,13 +860,14 @@ let vernac_cofixpoint_interactive ~atts discharge l =
     CErrors.user_err Pp.(str"Program CoFixpoint requires a body");
   ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l
 
-let vernac_cofixpoint ~atts discharge l =
+let vernac_cofixpoint ~atts ~pm discharge l =
   let open DefAttributes in
   let scope = vernac_cofixpoint_common ~atts discharge l in
   if atts.program then
-    ComProgramFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l
+    ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic l
   else
-    ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l
+    let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l in
+    pm
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1085,10 +1088,10 @@ let msg_of_subsection ss id =
   in
   Pp.str kind ++ spc () ++ Id.print id
 
-let vernac_end_segment ({v=id} as lid) =
+let vernac_end_segment ~pm ({v=id} as lid) =
   let ss = Lib.find_opening_node id in
   let what_for = msg_of_subsection ss lid.v in
-  Declare.Obls.check_solved_obligations ~what_for;
+  Declare.Obls.check_solved_obligations ~pm ~what_for;
   match ss with
   | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
   | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
@@ -1147,14 +1150,14 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance_program ~atts name bl t props info =
+let vernac_instance_program ~atts ~pm name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
   let locality, poly =
     Attributes.(parse (Notations.(locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
-  let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in
-  ()
+  let pm, _id = Classes.new_instance_program ~pm ~global ~poly name bl t props info in
+  pm
 
 let vernac_instance_interactive ~atts name bl t info props =
   Dumpglob.dump_constraint (fst name) false "inst";
@@ -1991,9 +1994,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
   (* Gallina *)
 
   | VernacDefinition (discharge,lid,DefineBody (bl,red_option,c,typ)) ->
-    VtDefault (fun () ->
+    VtModifyProgram (fun ~pm ->
       with_def_attributes ~atts
-       vernac_definition discharge lid bl red_option c typ)
+       vernac_definition ~pm discharge lid bl red_option c typ)
   | VernacDefinition (discharge,lid,ProveBody(bl,typ)) ->
     VtOpenProof(fun () ->
       with_def_attributes ~atts
@@ -2028,14 +2031,14 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
       VtOpenProof (fun () ->
         with_def_attributes ~atts vernac_fixpoint_interactive discharge l)
     else
-      VtDefault (fun () ->
-        with_def_attributes ~atts vernac_fixpoint discharge l)
+      VtModifyProgram (fun ~pm ->
+        with_def_attributes ~atts (vernac_fixpoint ~pm) discharge l)
   | VernacCoFixpoint (discharge, l) ->
     let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in
     if opens then
       VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l)
     else
-      VtDefault(fun () -> with_def_attributes ~atts vernac_cofixpoint discharge l)
+      VtModifyProgram(fun ~pm -> with_def_attributes ~atts (vernac_cofixpoint ~pm) discharge l)
 
   | VernacScheme l ->
     VtDefault(fun () ->
@@ -2064,9 +2067,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
     VtNoProof(fun () ->
         vernac_begin_section ~poly:(only_polymorphism atts) lid)
   | VernacEndSegment lid ->
-    VtNoProof(fun () ->
+    VtReadProgram(fun ~pm ->
         unsupported_attributes atts;
-        vernac_end_segment lid)
+        vernac_end_segment ~pm lid)
   | VernacNameSectionHypSet (lid, set) ->
     VtDefault(fun () ->
         unsupported_attributes atts;
@@ -2091,7 +2094,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacInstance (name, bl, t, props, info) ->
     let atts, program = Attributes.(parse_with_extra program) atts in
     if program then
-      VtDefault (fun () -> vernac_instance_program ~atts name bl t props info)
+      VtModifyProgram (vernac_instance_program ~atts name bl t props info)
     else begin match props with
     | None ->
        VtOpenProof (fun () ->
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index f8a80e8feb..496b1a43d1 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -55,11 +55,15 @@ and proof_block_name = string (** open type of delimiters *)
 type typed_vernac =
   | VtDefault of (unit -> unit)
   | VtNoProof of (unit -> unit)
-  | VtCloseProof of (lemma:Declare.Proof.t -> unit)
+  | VtCloseProof of (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t)
   | VtOpenProof of (unit -> Declare.Proof.t)
   | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
   | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
   | VtReadProof of (pstate:Declare.Proof.t -> unit)
+  | VtReadProgram of (pm:Declare.OblState.t -> unit)
+  | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t)
+  | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
+  | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
 
 type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 103e24233b..5ef137cfc0 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -73,11 +73,15 @@ and proof_block_name = string (** open type of delimiters *)
 type typed_vernac =
   | VtDefault of (unit -> unit)
   | VtNoProof of (unit -> unit)
-  | VtCloseProof of (lemma:Declare.Proof.t -> unit)
+  | VtCloseProof of (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t)
   | VtOpenProof of (unit -> Declare.Proof.t)
   | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
   | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
   | VtReadProof of (pstate:Declare.Proof.t -> unit)
+  | VtReadProgram of (pm:Declare.OblState.t -> unit)
+  | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t)
+  | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
+  | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
 
 type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1b977b8e10..6be2fb0d43 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -22,32 +22,41 @@ let vernac_require_open_lemma ~stack f =
   | None ->
     CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress)")
 
-let interp_typed_vernac c ~stack =
+let interp_typed_vernac c ~pm ~stack =
   let open Vernacextend in
   match c with
-  | VtDefault f -> f (); stack
+  | VtDefault f -> f (); stack, pm
   | VtNoProof f ->
     if Option.has_some stack then
       CErrors.user_err (Pp.str "Command not supported (Open proofs remain)");
     let () = f () in
-    stack
+    stack, pm
   | VtCloseProof f ->
     vernac_require_open_lemma ~stack (fun stack ->
         let lemma, stack = Vernacstate.LemmaStack.pop stack in
-        f ~lemma;
-        stack)
+        let pm = f ~lemma ~pm in
+        stack, pm)
   | VtOpenProof f ->
-    Some (Vernacstate.LemmaStack.push stack (f ()))
+    Some (Vernacstate.LemmaStack.push stack (f ())), pm
   | VtModifyProof f ->
-    Option.map (Vernacstate.LemmaStack.map_top ~f:(fun pstate -> f ~pstate)) stack
+    Option.map (Vernacstate.LemmaStack.map_top ~f:(fun pstate -> f ~pstate)) stack, pm
   | VtReadProofOpt f ->
     let pstate = Option.map (Vernacstate.LemmaStack.with_top ~f:(fun x -> x)) stack in
     f ~pstate;
-    stack
+    stack, pm
   | VtReadProof f ->
     vernac_require_open_lemma ~stack
       (Vernacstate.LemmaStack.with_top ~f:(fun pstate -> f ~pstate));
-    stack
+    stack, pm
+  | VtReadProgram f -> f ~pm; stack, pm
+  | VtModifyProgram f ->
+    let pm = f ~pm in stack, pm
+  | VtDeclareProgram f ->
+    let lemma = f ~pm in
+    Some (Vernacstate.LemmaStack.push stack lemma), pm
+  | VtOpenProofProgram f ->
+    let pm, lemma = f ~pm in
+    Some (Vernacstate.LemmaStack.push stack lemma), pm
 
 (* Default proof mode, to be set at the beginning of proofs for
    programs that cannot be statically classified. *)
@@ -123,11 +132,11 @@ let mk_time_header =
   fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac)
 
 let interp_control_flag ~time_header (f : control_flag) ~st
-    (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) =
+    (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option * Declare.OblState.t) =
   match f with
   | ControlFail ->
     with_fail ~st (fun () -> fn ~st);
-    st.Vernacstate.lemmas
+    st.Vernacstate.lemmas, st.Vernacstate.program
   | ControlTimeout timeout ->
     vernac_timeout ~timeout (fun () -> fn ~st) ()
   | ControlTime batch ->
@@ -142,6 +151,7 @@ let interp_control_flag ~time_header (f : control_flag) ~st
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let rec interp_expr ~atts ~st c =
   let stack = st.Vernacstate.lemmas in
+  let program = st.Vernacstate.program in
   vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
 
@@ -163,7 +173,7 @@ let rec interp_expr ~atts ~st c =
     vernac_load ~verbosely fname
   | v ->
     let fv = Vernacentries.translate_vernac ~atts v in
-    interp_typed_vernac ~stack fv
+    interp_typed_vernac ~pm:program ~stack fv
 
 and vernac_load ~verbosely fname =
   (* Note that no proof should be open here, so the state here is just token for now *)
@@ -180,19 +190,19 @@ and vernac_load ~verbosely fname =
   let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
       (Pcoq.Entry.parse (Pvernac.main_entry proof_mode))
   in
-  let rec load_loop ~stack =
+  let rec load_loop ~pm ~stack =
     let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
     match parse_sentence proof_mode input with
-    | None -> stack
+    | None -> stack, pm
     | Some stm ->
-      let stack = v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) stm in
-      (load_loop [@ocaml.tailcall]) ~stack
+      let stack, pm = v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack; program = pm }) stm in
+      (load_loop [@ocaml.tailcall]) ~stack ~pm
   in
-  let stack = load_loop ~stack:st.Vernacstate.lemmas in
+  let stack, pm = load_loop ~pm:st.Vernacstate.program ~stack:st.Vernacstate.lemmas in
   (* If Load left a proof open, we fail too. *)
   if Option.has_some stack then
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
-  stack
+  stack, pm
 
 and interp_control ~st ({ CAst.v = cmd } as vernac) =
   let time_header = mk_time_header vernac in
@@ -200,9 +210,9 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
     cmd.control
     (fun ~st ->
        let before_univs = Global.universes () in
-       let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
-       if before_univs == Global.universes () then pstack
-       else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack)
+       let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in
+       if before_univs == Global.universes () then pstack, pm
+       else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack, pm)
     ~st
 
 (* XXX: This won't properly set the proof mode, as of today, it is
@@ -213,17 +223,18 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
 *)
 
 (* Interpreting a possibly delayed proof *)
-let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option =
+let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t =
   let stack = st.Vernacstate.lemmas in
+  let pm = st.Vernacstate.program in
   let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
-  let () = match pe with
+  let pm = match pe with
     | Admitted ->
-      Declare.Proof.save_lemma_admitted_delayed ~proof ~pinfo
+      Declare.Proof.save_lemma_admitted_delayed ~pm ~proof ~pinfo
     | Proved (_,idopt) ->
-      let _ : _ list = Declare.Proof.save_lemma_proved_delayed ~proof ~pinfo ~idopt in
-      ()
+      let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt in
+      pm
   in
-  stack
+  stack, pm
 
 let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } =
   let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 073ef1c2d7..ee06205427 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -113,15 +113,18 @@ type t = {
   parsing : Parser.t;
   system  : System.t;              (* summary + libstack *)
   lemmas  : LemmaStack.t option;   (* proofs of lemmas currently opened *)
+  program : Declare.OblState.t;    (* obligations table *)
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
 let s_cache = ref None
 let s_lemmas = ref None
+let s_program = ref Declare.OblState.empty
 
 let invalidate_cache () =
   s_cache := None;
-  s_lemmas := None
+  s_lemmas := None;
+  s_program := Declare.OblState.empty
 
 let update_cache rf v =
   rf := Some v; v
@@ -138,20 +141,24 @@ let do_if_not_cached rf f v =
 let freeze_interp_state ~marshallable =
   { system = update_cache s_cache (System.freeze ~marshallable);
     lemmas = !s_lemmas;
+    program = !s_program;
     shallow = false;
     parsing = Parser.cur_state ();
   }
 
-let unfreeze_interp_state { system; lemmas; parsing } =
+let unfreeze_interp_state { system; lemmas; program; parsing } =
   do_if_not_cached s_cache System.unfreeze system;
   s_lemmas := lemmas;
+  s_program := program;
   Pcoq.unfreeze parsing
 
 (* Compatibility module *)
 module Declare_ = struct
 
   let get () = !s_lemmas
-  let set x = s_lemmas := x
+  let set (pstate,pm) =
+    s_lemmas := pstate;
+    s_program := pm
 
   let get_pstate () =
     Option.map (LemmaStack.with_top ~f:(fun x -> x)) !s_lemmas
@@ -237,18 +244,16 @@ module Stm = struct
   type nonrec pstate =
     LemmaStack.t option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
-    int *                                   (* Evd.evar_counter_summary_tag *)
-    Declare.Obls.State.t
+    int                                     (* Evd.evar_counter_summary_tag *)
 
   (* Parts of the system state that are morally part of the proof state *)
   let pstate { lemmas; system } =
     let st = System.Stm.summary system in
     lemmas,
     Summary.project_from_summary st Evarutil.meta_counter_summary_tag,
-    Summary.project_from_summary st Evd.evar_counter_summary_tag,
-    Summary.project_from_summary st Declare.Obls.State.prg_tag
+    Summary.project_from_summary st Evd.evar_counter_summary_tag
 
-  let set_pstate ({ lemmas; system } as s) (pstate,c1,c2,c3) =
+  let set_pstate ({ lemmas; system } as s) (pstate,c1,c2) =
     { s with
       lemmas =
         Declare_.copy_terminators ~src:s.lemmas ~tgt:pstate
@@ -258,7 +263,6 @@ module Stm = struct
             let st = System.Stm.summary s.system in
             let st = Summary.modify_summary st Evarutil.meta_counter_summary_tag c1 in
             let st = Summary.modify_summary st Evd.evar_counter_summary_tag c2 in
-            let st = Summary.modify_summary st Declare.Obls.State.prg_tag c3 in
             st
           end
       }
@@ -267,7 +271,6 @@ module Stm = struct
     let st = System.Stm.summary system in
     let st = Summary.remove_from_summary st Evarutil.meta_counter_summary_tag in
     let st = Summary.remove_from_summary st Evd.evar_counter_summary_tag in
-    let st = Summary.remove_from_summary st Declare.Obls.State.prg_tag in
     st, System.Stm.lib system
 
   let same_env { system = s1 } { system = s2 } =
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 8c23ac0698..16fab3782b 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -52,6 +52,8 @@ type t =
   (** summary + libstack *)
   ; lemmas  : LemmaStack.t option
   (** proofs of lemmas currently opened *)
+  ; program : Declare.OblState.t
+  (** program mode table *)
   ; shallow : bool
   (** is the state trimmed down (libstack) *)
   }
@@ -112,7 +114,7 @@ module Declare : sig
 
   (* Low-level stuff *)
   val get : unit -> LemmaStack.t option
-  val set : LemmaStack.t option -> unit
+  val set : LemmaStack.t option * Declare.OblState.t -> unit
 
   val get_pstate : unit -> Declare.Proof.t option