diff options
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 69e2a209eb..6296347fd0 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -248,7 +248,7 @@ let collect_evars_of_term evd c ty = evars (Evd.from_ctx (Evd.evar_universe_context evd)) let do_program_recursive local poly fixkind fixl ntns = - let cofix = fixkind = Obligations.IsCoFixpoint in + let cofix = fixkind = DeclareObl.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl ntns in @@ -289,8 +289,8 @@ let do_program_recursive local poly fixkind fixl ntns = end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with - | Obligations.IsFixpoint _ -> (local, poly, Fixpoint) - | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint) + | DeclareObl.IsFixpoint _ -> (local, poly, Fixpoint) + | DeclareObl.IsCoFixpoint -> (local, poly, CoFixpoint) in Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind @@ -316,7 +316,7 @@ let do_program_fixpoint local poly l = | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> let fixl,ntns = extract_fixpoint_components ~structonly:true l in - let fixkind = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in + let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in do_program_recursive local poly fixkind fixl ntns | _, _ -> @@ -341,5 +341,5 @@ let do_fixpoint local poly l = let do_cofixpoint local poly l = let fixl,ntns = extract_cofixpoint_components l in - do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns; + do_program_recursive local poly DeclareObl.IsCoFixpoint fixl ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () |