5 files changed, 8 insertions, 64 deletions
diff --git a/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst b/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst
new file mode 100644
index 0000000000..84d6bdea89
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  The Hide Obligations flag, deprecated in 8.12
+  (`#13758 <https://github.com/coq/coq/pull/13758>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 2b24ced8a1..8f2b51ccce 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -320,14 +320,6 @@ optional tactic is replaced by the default one if not specified.
    (the default), or if the system should infer which obligations can be
    declared opaque.
 
-.. flag:: Hide Obligations
-
-   .. deprecated:: 8.12
-
-   Controls whether obligations appearing in the
-   term should be hidden as implicit arguments of the special
-   constant ``Program.Tactics.obligation``.
-
 The module :g:`Coq.Program.Tactics` defines the default tactic for solving
 obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also
 adds some useful notations, as documented in the file itself.
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index d9e4e4f2b3..fc40ba0249 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -1230,7 +1230,7 @@ Flags, options and attributes
   :attr:`universes(template)` and ``universes(notemplate)`` instead
   (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann).
 - **Deprecated:**
-  :flag:`Hide Obligations` flag
+  `Hide Obligations` flag
   (`#11828 <https://github.com/coq/coq/pull/11828>`_,
   by Emilio Jesus Gallego Arias).
 - **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index fce69437d7..d852ad24fe 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -319,7 +319,3 @@ Create HintDb program discriminated.
 Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf.
 
 Obligation Tactic := program_simpl.
-
-Definition obligation (A : Type) {a : A} := a.
-
-Register obligation as program.tactics.obligation.
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c715304419..48aa329e5e 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -889,13 +889,6 @@ let add_hint local prg cst =
   let locality = if local then Goptions.OptLocal else Goptions.OptExport in
   Hints.add_hints ~locality [Id.to_string prg.prg_cinfo.CInfo.name] (unfold_entry cst)
 
-(* true = hide obligations *)
-let get_hide_obligations =
-  Goptions.declare_bool_option_and_ref
-    ~depr:true
-    ~key:["Hide"; "Obligations"]
-    ~value:false
-
 let declare_obligation prg obl ~uctx ~types ~body =
   let poly = prg.prg_info.Info.poly in
   let univs = UState.univ_entry ~poly uctx in
@@ -1046,51 +1039,10 @@ let obligation_substitution expand prg =
   let ints = intset_to (pred (Array.length obls)) in
   obl_substitution expand obls ints
 
-let hide_obligation () =
-  Coqlib.check_required_library ["Coq"; "Program"; "Tactics"];
-  UnivGen.constr_of_monomorphic_global
-    (Coqlib.lib_ref "program.tactics.obligation")
-
-(* XXX: Is this the right place? *)
-let rec prod_app t n =
-  match
-    Constr.kind
-      (EConstr.Unsafe.to_constr
-         (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t)))
-    (* FIXME *)
-  with
-  | Prod (_, _, b) -> Vars.subst1 n b
-  | LetIn (_, b, t, b') -> prod_app (Vars.subst1 b b') n
-  | _ ->
-    CErrors.user_err ~hdr:"prod_app"
-      Pp.(str "Needed a product, but didn't find one" ++ fnl ())
-
-(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_applist t nL = List.fold_left prod_app t nL
-
-let replace_appvars subst =
-  let rec aux c =
-    let f, l = decompose_app c in
-    if isVar f then
-      try
-        let c' = List.map (Constr.map aux) l in
-        let t, b = Id.List.assoc (destVar f) subst in
-        mkApp
-          ( delayed_force hide_obligation
-          , [|prod_applist t c'; Term.applistc b c'|] )
-      with Not_found -> Constr.map aux c
-    else Constr.map aux c
-  in
-  Constr.map aux
-
 let subst_prog subst prg =
-  if get_hide_obligations () then
-    ( replace_appvars subst prg.prg_body
-    , replace_appvars subst (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
-  else
-    let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
-    ( Vars.replace_vars subst' prg.prg_body
-    , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
+  let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
+  ( Vars.replace_vars subst' prg.prg_body
+  , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
 
 let declare_definition ~pm prg =
   let varsubst = obligation_substitution true prg in