diff options
| -rw-r--r-- | vernac/comFixpoint.ml | 16 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 5 | ||||
| -rw-r--r-- | vernac/declareDef.mli | 13 | ||||
| -rw-r--r-- | vernac/declareObl.ml | 15 |
4 files changed, 16 insertions, 33 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a29d60ccde..65dffb3c0b 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -272,8 +272,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = let indexes, cofix, fix_kind = match indexes with - | Some indexes -> indexes, false, Decls.Fixpoint - | None -> [], true, Decls.CoFixpoint + | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint) + | None -> [], true, Decls.(IsDefinition CoFixpoint) in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -294,11 +294,13 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in - let fixdecls = List.map mk_pure fixdecls in - ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx) - fixnames fixdecls fixtypes fiximps); + let udecl = Evd.universe_binders evd in + let _ : GlobRef.t list = + List.map4 (fun name body types imps -> + let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in + DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps) + fixnames fixdecls fixtypes fiximps + in recursive_message (not cofix) gidx fixnames; List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; () diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index dea2ccb9af..39fd332184 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,11 +69,6 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = end; dref -let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - let kind = Decls.IsDefinition kind in - declare_definition ~name ~scope ~kind ?hook_data udecl ce imps - let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 17c2862cad..c668ab2ac4 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -49,19 +49,6 @@ val declare_definition -> Impargs.manual_implicits -> GlobRef.t -val declare_fix - : ?opaque:bool - -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> name:Id.t - -> scope:locality - -> kind:Decls.definition_object_kind - -> UnivNames.universe_binders - -> Entries.universes_entry - -> Evd.side_effects Entries.proof_output - -> Constr.types - -> Impargs.manual_implicits - -> GlobRef.t - val declare_assumption : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> name:Id.t diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index dcb28b898f..eb9b896ec6 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -376,9 +376,6 @@ let compute_possible_guardness_evidences n fixbody fixtype = let ctx = fst (Term.decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx -let mk_proof c = - ((c, Univ.ContextSet.empty), Evd.empty_side_effects) - let declare_mutual_definition l = let len = List.length l in let first = List.hd l in @@ -410,7 +407,6 @@ let declare_mutual_definition l = let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in let fixnames = first.prg_deps in let opaque = first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint in let indexes, fixdecls = match fixkind with | IsFixpoint wfl -> @@ -421,20 +417,23 @@ let declare_mutual_definition l = Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in ( Some indexes - , List.map_i (fun i _ -> mk_proof (mkFix ((indexes, i), fixdecls))) 0 l + , List.map_i (fun i _ -> mkFix ((indexes, i), fixdecls)) 0 l ) | IsCoFixpoint -> - (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l) + (None, List.map_i (fun i _ -> mkCoFix (i, fixdecls)) 0 l) in (* Declare the recursive definitions *) let poly = first.prg_poly in let scope = first.prg_scope in let univs = UState.univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in + let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in + let udecl = UnivNames.empty_binders in let kns = List.map4 - (fun name -> DeclareDef.declare_fix ~name ~opaque ~scope ~kind - UnivNames.empty_binders univs) + (fun name body types imps -> + let ce = Declare.definition_entry ~opaque ~types ~univs body in + DeclareDef.declare_definition ~name ~scope ~kind udecl ce imps) fixnames fixdecls fixtypes fiximps in (* Declare notations *) |