diff options
| author | Gaëtan Gilbert | 2020-03-31 11:05:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 11:05:21 +0200 |
| commit | 29bcd98d55ccb9a90dff7fc8f254578c4d870a09 (patch) | |
| tree | c87bee672d196212e4f0033804e57c00deadeef8 /vernac/comFixpoint.mli | |
| parent | c31a634b1f57028f3491b61137e53978d2653bbe (diff) | |
| parent | 1320d5004b58f33c2274bfdc0629d7f513cd49c4 (diff) | |
Merge PR #11818: [proof] Further consolidation of the regular declaration path
Ack-by: Matafou
Reviewed-by: SkySkimmer
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 *) |