From 5da15336a01d1f74fac653f69cd0a509ba05a3ab Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 05:24:03 -0400
Subject: [comFixpoint] Minor cleanups in type declarations.

---
 vernac/comFixpoint.mli | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'vernac/comFixpoint.mli')

diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 2ad6c03bae..a19b96f0f3 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Vernacexpr
 
 (** {6 Fixpoints and cofixpoints} *)
@@ -40,6 +39,9 @@ val adjust_rec_order
   -> Constrexpr.recursion_order_expr option
   -> lident option
 
+(** names / relevance / defs / types *)
+type ('constr, 'types) recursive_preentry = Id.t list * Sorts.relevance list * 'constr option list * 'types list
+
 (** Exported for Program *)
 val interp_recursive :
   (* Misc arguments *)
@@ -49,18 +51,17 @@ val interp_recursive :
   (* env / signature / univs / evar_map *)
   (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
-  (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
+  (EConstr.t, EConstr.types) recursive_preentry *
   (* ctx per mutual def / implicits / struct annotations *)
   (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Exported for Funind *)
 
-type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list
-
 val interp_fixpoint
   :  cofix:bool
   -> lident option fix_expr_gen list
-  -> recursive_preentry * UState.universe_decl * UState.t *
+  -> (Constr.t, Constr.types) recursive_preentry *
+     UState.universe_decl * UState.t *
      (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Very private function, do not use *)
-- 
cgit v1.2.3