[obligations] Use already existing type alias.

Simple cleanup: we make use of the `obligation_info` type alias in the
function generating it.

1 files changed, 25 insertions, 19 deletions

diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index f97bc784c3..3bffdb5f52 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -18,27 +18,33 @@ val check_evars : env -> evar_map -> unit
 val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t
 val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list
 
-(* env, id, evars, number of function prototypes to try to clear from
-   evars contexts, object and type *)
-val eterm_obligations : env -> Id.t -> evar_map -> int ->
-  ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types ->
-  (Id.t * types * Evar_kinds.t Loc.located *
-     (bool * Evar_kinds.obligation_definition_status) * Int.Set.t *
-      unit Proofview.tactic option) array
-    (* Existential key, obl. name, type as product, 
-       location of the original evar, associated tactic,
-       status and dependencies as indexes into the array *)
-  * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) *
-    constr * types
-    (* Translations from existential identifiers to obligation identifiers 
-       and for terms with existentials to closed terms, given a 
-       translation from obligation identifiers to constrs, new term, new type *)
-
+(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *)
 type obligation_info =
   (Id.t * types * Evar_kinds.t Loc.located *
-      (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array
-    (* ident, type, location, (opaque or transparent, expand or define),
-       dependencies, tactic to solve it *)
+   (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array
+
+(* env, id, evars, number of function prototypes to try to clear from
+   evars contexts, object and type *)
+val eterm_obligations
+  :  env
+  -> Id.t
+  -> evar_map
+  -> int
+  -> ?status:Evar_kinds.obligation_definition_status
+  -> EConstr.constr
+  -> EConstr.types
+  -> obligation_info *
+
+     (* Existential key, obl. name, type as product, location of the
+        original evar, associated tactic, status and dependencies as
+        indexes into the array *)
+     ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) *
+
+     (* Translations from existential identifiers to obligation
+        identifiers and for terms with existentials to closed terms,
+        given a translation from obligation identifiers to constrs,
+        new term, new type *)
+     constr * types
 
 val default_tactic : unit Proofview.tactic ref