diff options
| -rw-r--r-- | vernac/comFixpoint.ml | 16 | ||||
| -rw-r--r-- | vernac/comFixpoint.mli | 11 |
2 files changed, 17 insertions, 10 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 6580495295..cbf0affc12 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -140,8 +140,8 @@ let compute_possible_guardness_evidences (ctx,_,recindex) = fixpoints ?) *) List.interval 0 (Context.Rel.nhyps ctx - 1) -type recursive_preentry = - Id.t list * Sorts.relevance list * Constr.t option list * Constr.types list +type ('constr, 'types) recursive_preentry = + Id.t list * Sorts.relevance list * 'constr option list * 'types list (* Wellfounded definition *) @@ -230,7 +230,11 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) -let interp_fixpoint ~cofix l = +(* XXX: Unify with interp_recursive *) +let interp_fixpoint ~cofix l : + ( (Constr.t, Constr.types) recursive_preentry * + UState.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list) = let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in check_recursive true env evd fix; let uctx,fix = ground_fixpoint env evd fix in @@ -243,8 +247,10 @@ let build_recthms ~indexes fixnames fixtypes fiximps = in let thms = List.map3 (fun name typ (ctx,impargs,_) -> - { DeclareDef.Recthm.name; typ - ; args = List.map Context.Rel.Declaration.get_name ctx; impargs}) + { DeclareDef.Recthm.name + ; typ + ; args = List.map Context.Rel.Declaration.get_name ctx + ; impargs}) fixnames fixtypes fiximps in fix_kind, cofix, thms 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 *) |