diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 05:24:03 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:36 -0400 |
| commit | 5da15336a01d1f74fac653f69cd0a509ba05a3ab (patch) | |
| tree | 478b37746053fafec63ed0d0ca82db54bdf8073a /vernac/comFixpoint.mli | |
| parent | dc71c61e76b4ffff09b8d41e69ae403348e064fe (diff) | |
[comFixpoint] Minor cleanups in type declarations.
Diffstat (limited to 'vernac/comFixpoint.mli')
| -rw-r--r-- | vernac/comFixpoint.mli | 11 |
1 files changed, 6 insertions, 5 deletions
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 *) |