diff options
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 21 |
1 files changed, 5 insertions, 16 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index ced9656218..6e6be4fe3a 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -256,26 +256,15 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs lemma let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - let indexes, cofix, fix_kind = + let possible_indexes, cofix, fix_kind = match indexes with - | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint) - | None -> [], true, Decls.(IsDefinition CoFixpoint) + | Some indexes -> Some indexes, false, Decls.(IsDefinition Fixpoint) + | None -> None, true, Decls.(IsDefinition CoFixpoint) in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let vars, fixdecls, indexes = - if not cofix then - let env = Global.env() in - let indexes = Pretyping.search_guard env indexes fixdecls in - let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),fixdecls)) in - let fixdecls = List.map_i (fun i _ -> Constr.mkFix ((indexes,i),fixdecls)) 0 fixnames in - vars, fixdecls, Some indexes - else (* cofix *) - let fixdecls = List.map_i (fun i _ -> Constr.mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Vars.universes_of_constr (List.hd fixdecls) in - vars, fixdecls, None - in + let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in + let vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in let fiximps = List.map (fun (n,r,p) -> r) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in |