diff options
| author | Gaëtan Gilbert | 2020-05-19 14:12:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-19 14:12:30 +0200 |
| commit | 407ca661d7eb33afed706afe74f11fccac2f1dd4 (patch) | |
| tree | d867bc7f77bfeb1c9a09598f7945d7d77f1ccae3 /vernac/comProgramFixpoint.ml | |
| parent | 2222e455f0501b700f198ab614d8743229062f73 (diff) | |
| parent | 833d7672a4cc1dbdd4ab5a861362824b03f72d57 (diff) | |
Merge PR #12301: [declare] Grand unification of the proof save path.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
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 4e9e24b119..4aa46e0a86 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty = evars (Evd.from_ctx (Evd.evar_universe_context evd)) let do_program_recursive ~scope ~poly fixkind fixl = - let cofix = fixkind = DeclareObl.IsCoFixpoint in + let cofix = fixkind = Declare.Obls.IsCoFixpoint in let (env, rec_sign, udecl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl in @@ -314,8 +314,8 @@ let do_program_recursive ~scope ~poly fixkind fixl = end in let uctx = Evd.evar_universe_context evd in let kind = match fixkind with - | DeclareObl.IsFixpoint _ -> Decls.Fixpoint - | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint + | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint + | Declare.Obls.IsCoFixpoint -> Decls.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 @@ -345,7 +345,7 @@ let do_fixpoint ~scope ~poly l = | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> let annots = List.map (fun fix -> Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in - let fixkind = DeclareObl.IsFixpoint annots in + let fixkind = Declare.Obls.IsFixpoint annots in let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in do_program_recursive ~scope ~poly fixkind l @@ -355,4 +355,4 @@ let do_fixpoint ~scope ~poly l = let do_cofixpoint ~scope ~poly fixl = let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in - do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl + do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl |