[declare] Some more cleanup on unused functions after the last commits.

5 files changed, 14 insertions, 20 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index f02474a405..ba08aa2b94 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -349,7 +349,7 @@ 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.progress =
+  let _ : Declare.Obls.progress =
     Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls
   in ()
 
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5860626917..f9b2d8b1d1 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -128,7 +128,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
     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.progress =
+  let _ : Declare.Obls.progress =
     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
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index b04aaa7e6f..37615fa09c 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -262,7 +262,8 @@ 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.progress = Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in
+  let _ : Declare.Obls.progress =
+    Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in
   ()
 
 let out_def = function
diff --git a/vernac/declare.ml b/vernac/declare.ml
index d170e084d4..705a136a67 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -2513,5 +2513,7 @@ let prepare_obligation = prepare_obligation
 let check_solved_obligations = Obls_.check_solved_obligations
 type fixpoint_kind = Obls_.fixpoint_kind =
   | IsFixpoint of lident option list | IsCoFixpoint
+type nonrec progress = progress =
+  | Remain of int | Dependent | Defined of GlobRef.t
 
 end
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 55bbcb9e1e..dc1c28edce 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -79,12 +79,11 @@ module CInfo : sig
     -> unit
     -> 'constr t
 
-  (* Eventually we would like to remove the constr parameter *)
+  (* Used only in Vernacentries, may disappear from public API *)
   val to_constr : Evd.evar_map -> EConstr.t t -> Constr.t t
 
+  (* Used only in RecLemmas, may disappear from public API *)
   val get_typ : 'constr t -> 'constr
-  (* To be removed once obligations are merged here *)
-  val get_name : 'constr t -> Id.t
 
 end
 
@@ -148,20 +147,6 @@ val declare_mutually_recursive
 
 (** {2 Declaration of interactive constants }  *)
 
-(** Resolution status of a program *)
-type progress =
-  | Remain of int  (** n obligations remaining *)
-  | Dependent  (** Dependent on other definitions *)
-  | Defined of GlobRef.t  (** Defined as id *)
-
-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}
-
 (** [Declare.Proof.t] Construction of constants using interactive proofs. *)
 module Proof : sig
 
@@ -473,6 +458,12 @@ val check_solved_obligations : what_for:Pp.t -> unit
 
 val default_tactic : unit Proofview.tactic ref
 
+(** Resolution status of a program *)
+type progress =
+  | Remain of int  (** n obligations remaining *)
+  | Dependent  (** Dependent on other definitions *)
+  | Defined of GlobRef.t  (** Defined as id *)
+
 (** Prepare API, to be removed once we provide the corresponding 1-step API *)
 val prepare_obligation
   :  name:Id.t