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.ml | |
| parent | dc71c61e76b4ffff09b8d41e69ae403348e064fe (diff) | |
[comFixpoint] Minor cleanups in type declarations.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 16 |
1 files changed, 11 insertions, 5 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 |