diff options
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 87aa5d9b2d..381b6cb9fa 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -260,8 +260,10 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = RetrieveObl.retrieve_obligations env recname sigma 0 def typ in let uctx = Evd.evar_universe_context sigma in - ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl - ~poly evars_typ ~uctx evars ~hook) + let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in + let info = Declare.Info.make ~udecl ~poly ~hook () in + let _ : Declare.progress = Obligations.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in + () let out_def = function | Some def -> def @@ -319,7 +321,8 @@ let do_program_recursive ~scope ~poly fixkind fixl = | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint) in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in - Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind + let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in + Obligations.add_mutual_definitions defs ~info ~uctx ~ntns fixkind let do_fixpoint ~scope ~poly l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in |