diff --git a/doc/changelog/02-specification-language/19257-master+merge-fixpoint-program-fixpoint.rst b/doc/changelog/02-specification-language/19257-master+merge-fixpoint-program-fixpoint.rst new file mode 100644 index 000000000000..daa747fd2e41 --- /dev/null +++ b/doc/changelog/02-specification-language/19257-master+merge-fixpoint-program-fixpoint.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Mishandling of let binders in `Program Fixpoint` + (`#19257 `_, + fixes `#16906 `_, + by Hugo Herbelin). diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index b34207c00f53..5a5cec7f1354 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -153,9 +153,7 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (rec_order, fixpoint_exprl) = - let _, _, ((_, _, _, typel), _, uctx, _) = - ComFixpoint.interp_recursive ~check_recursivity:false (false, CFixRecOrder rec_order) fixpoint_exprl - in + let typel, uctx = ComFixpoint.interp_fixpoint_short rec_order fixpoint_exprl in let constr_expr_typel = with_full_print (List.map (fun c -> @@ -406,8 +404,8 @@ let register_struct is_rec (rec_order, fixpoint_exprl) = in (None, evd, List.rev rev_pconstants) | _ -> - let p = ComFixpoint.do_mutually_recursive ~poly:false (CFixRecOrder rec_order, fixpoint_exprl) in - assert (Option.is_empty p); + let pm, p = ComFixpoint.do_mutually_recursive ~poly:false (CFixRecOrder rec_order, fixpoint_exprl) in + assert (Option.is_empty pm && Option.is_empty p); let evd, rev_pconstants = List.fold_left (fun (evd, l) {Vernacexpr.fname} -> diff --git a/test-suite/bugs/bug_16906.v b/test-suite/bugs/bug_16906.v new file mode 100644 index 000000000000..e0b315b100d9 --- /dev/null +++ b/test-suite/bugs/bug_16906.v @@ -0,0 +1,8 @@ +Require Import Coq.Program.Program. +Require Import Coq.Lists.List. +Import ListNotations. +Open Scope list_scope. +Program Fixpoint foo + (_local_inst := tt) (decls : list unit) {struct decls} : list unit + := match decls with | [] => [] | _ => [] end. +(* Was raising a Not_found *) diff --git a/test-suite/success/ProgramFixpoint.v b/test-suite/success/ProgramFixpoint.v new file mode 100644 index 000000000000..c97b03c9a7bc --- /dev/null +++ b/test-suite/success/ProgramFixpoint.v @@ -0,0 +1,22 @@ +Require Import Program. + +Module ProgramFixProto. + +(* Check the presence of [fix_proto] so that a preliminary work done on + obligations can be done automatically *) + +Program Fixpoint do_bug m : { k : nat | exists u : nat, k = m } := + match m with + | 0 => 0 + | S m' => S (do_bug m') + end. +Next Obligation. + exists 0. + reflexivity. +Qed. +Next Obligation. + exists 0. + reflexivity. +Defined. + +End ProgramFixProto. diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 583e4adc0821..a51f6ffdca55 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -130,7 +130,7 @@ let adjust_rec_order ~structonly binders rec_order = (* Interpret the index of a recursion order annotation *) exception Found of int -let find_rec_annot ~structonly Vernacexpr.{fname={CAst.loc}; binders} (_, ctx) = function +let find_rec_annot ~structonly Vernacexpr.{fname={CAst.loc}; binders} ctx = function | None -> if Int.equal (Context.Rel.nhyps ctx) 0 then CErrors.user_err ?loc Pp.(str "A fixpoint needs at least one parameter."); List.interval 0 (Context.Rel.nhyps ctx - 1) @@ -169,34 +169,54 @@ let interp_rec_annot fixl ctxl (structonly, rec_order) = let interp_fix_context ~program_mode env sigma {Vernacexpr.binders} = let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma binders in - sigma, ((env', ctx), (impl_env, imps)) + sigma, (env', ctx, impl_env, imps) -let interp_fix_ccl ~program_mode sigma impls (env,_) fix = +let interp_fix_ccl ~program_mode sigma impls env fix = let flags = Pretyping.{ all_no_fail_flags with program_mode } in let sigma, (c, impl) = interp_type_evars_impls ~flags ~impls env sigma fix.Vernacexpr.rtype in let r = Retyping.relevance_of_type env sigma c in sigma, (c, r, impl) -let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl = +let interp_fix_body ~program_mode env_rec sigma impls ctx fix ccl = let open EConstr in Option.cata (fun body -> let env = push_rel_context ctx env_rec in let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.Vernacexpr.body_def -let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx +let build_fix_type sigma ctx ccl = + Evarutil.nf_evar sigma (EConstr.it_mkProd_or_LetIn ccl ctx) (* Jump over let-bindings. *) type ('constr, 'types, 'r) recursive_preentry = - Id.t list * 'r list * 'constr option list * 'types list + (Id.t list * 'r list * 'constr option list * 'types list * EConstr.rel_context list * Impargs.manual_implicits list) * + Decls.definition_object_kind * Pretyping.possible_guard * UState.universe_decl (* Wellfounded definition *) -let fix_proto sigma = - Evd.fresh_global (Global.env ()) sigma (Coqlib.lib_ref "program.tactic.fix_proto") -let fix_proto_relevance = EConstr.ERelevance.relevant -(* Would probably be overkill to use a specific fix_proto in SProp when in SProp?? *) +let encapsulate env sigma r t = + (* Would probably be overkill to use a specific fix_proto in SProp when in SProp?? *) + let fix_proto sigma = + Evd.fresh_global (Global.env ()) sigma (Coqlib.lib_ref "program.tactic.fix_proto") in + let fix_proto_relevance = EConstr.ERelevance.relevant in + let sigma, sort = Typing.type_of ~refresh:true env sigma t in + try + let sigma, h_term = fix_proto sigma in + let app = EConstr.mkApp (h_term, [|sort; t|]) in + let sigma, app = Typing.solve_evars env sigma app in + sigma, fix_proto_relevance, app + with e when CErrors.noncritical e -> sigma, r, t + +type ('constr, 'relevance) fix_data = { + fixnames : Names.Id.t list; + fixrs : 'relevance list; + fixdefs : 'constr option list; + fixtypes : 'constr list; + fixctxs : EConstr.rel_context list; + fiximps : (Names.Name.t * bool) option CAst.t list list; + fixntns : Metasyntax.notation_interpretation_decl list; +} let interp_recursive_evars env ~program_mode rec_order fixl = let open Context.Named.Declaration in @@ -205,33 +225,20 @@ let interp_recursive_evars env ~program_mode rec_order fixl = (* Interp arities allowing for unresolved types *) let sigma, decl = interp_mutual_univ_decl_opt env (List.map (fun Vernacexpr.{univs} -> univs) fixl) in - let sigma, (fixctxs, fiximppairs) = - on_snd List.split @@ + let sigma, (fixenv, fixctxs, fixctximpenvs, fixctximps) = + on_snd List.split4 @@ List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma) sigma fixl in - let fixkind, fixannot = interp_rec_annot fixl fixctxs rec_order in - let fixctximpenvs, fixctximps = List.split fiximppairs in + let fixkind, possible_guard = interp_rec_annot fixl fixctxs rec_order in let sigma, (fixccls,fixrs,fixcclimps) = on_snd List.split3 @@ - List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixctxs fixl in - let fixtypes = List.map2 build_fix_type fixctxs fixccls in - let fixtypes = List.map (fun c -> Evarutil.nf_evar sigma c) fixtypes in - let fiximps = List.map3 - (fun ctximps cclimps (_,ctx) -> ctximps@cclimps) - fixctximps fixcclimps fixctxs in + List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixenv fixl in + let fixtypes = List.map2 (build_fix_type sigma) fixctxs fixccls in + let fiximps = List.map2 (fun ctximps cclimps -> ctximps@cclimps) fixctximps fixcclimps in let sigma, rec_sign = List.fold_left3 (fun (sigma, env') id r t -> - if program_mode then - let sigma, sort = Typing.type_of ~refresh:true env sigma t in - let sigma, fixprot = - try - let sigma, h_term = fix_proto sigma in - let app = mkApp (h_term, [|sort; t|]) in - Typing.solve_evars env sigma app - with e when CErrors.noncritical e -> sigma, t - in - sigma, LocalAssum (Context.make_annot id fix_proto_relevance, fixprot) :: env' - else sigma, LocalAssum (Context.make_annot id r, t) :: env') + let sigma, r, t = if program_mode then encapsulate env sigma r t else sigma, r, t in + sigma, LocalAssum (Context.make_annot id r, t) :: env') (sigma,[]) fixnames fixrs fixtypes in let env_rec = push_named_context rec_sign env in @@ -240,10 +247,10 @@ let interp_recursive_evars env ~program_mode rec_order fixl = let impls = compute_internalization_env env sigma Recursive fixnames fixtypes fiximps in (* Interp bodies with rollback because temp use of notations/implicit *) + let fixntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in let sigma, fixdefs = Metasyntax.with_syntax_protection (fun () -> - let notations = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations) fixl in - List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; + List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) fixntns; List.fold_left4_map (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls)) sigma fixctximpenvs fixctxs fixl fixccls) @@ -252,63 +259,107 @@ let interp_recursive_evars env ~program_mode rec_order fixl = (* Instantiate evars and check all are resolved *) let sigma = Evarconv.solve_unif_constraints_with_heuristics env_rec sigma in let sigma = Evd.minimize_universes sigma in - let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in (* Build the fix declaration block *) - (env,rec_sign,decl,sigma), (fixnames,fixrs,fixdefs,fixtypes), List.combine fixctxs fiximps, fixkind, fixannot + let fix = {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns} in + (env, rec_sign, sigma), (fix, fixkind, possible_guard, decl) -let check_recursive ~isfix env evd (fixnames,_,fixdefs,_) = +let check_recursive ~isfix env evd {fixnames;fixdefs} = if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_true_recursivity env evd ~isfix (List.combine fixnames fixdefs) end -let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = +let ground_fixpoint env evd {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns} = Pretyping.check_evars_are_solved ~program_mode:false env evd; let fixrs = List.map (fun r -> EConstr.ERelevance.kind evd r) fixrs in let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in let fixtypes = List.map EConstr.(to_constr evd) fixtypes in - Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) + {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns} -(* XXX: Unify with interp_recursive *) -let interp_recursive ?(check_recursivity=true) ?typing_flags rec_order l : - Decls.definition_object_kind * Pretyping.possible_guard * ((Constr.t, Constr.types, Sorts.relevance) recursive_preentry * - UState.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits) list) = +(** For Funind *) + +let interp_fixpoint_short rec_order fixpoint_exprl = let env = Global.env () in - let env = Environ.update_typing_flags ?typing_flags env in - let (env,_,pl,evd),fix,info,isfix,possible_guards = interp_recursive_evars env ~program_mode:false rec_order l in - if check_recursivity then check_recursive ~isfix env evd fix; - let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in - let uctx,fix = ground_fixpoint env evd fix in - isfix, possible_guards, (fix,pl,uctx,info) - -let build_recthms fixnames fixtypes fiximps = - List.map3 (fun name typ (ctx,impargs) -> + let (_, _, sigma),(fix, _, _, _) = interp_recursive_evars env ~program_mode:false (false, CFixRecOrder rec_order) fixpoint_exprl in + let sigma = Pretyping.(solve_remaining_evars all_no_fail_flags env sigma) in + let typel = (ground_fixpoint env sigma fix).fixtypes in + let uctx = Evd.evar_universe_context sigma in + typel, uctx + +let build_recthms {fixnames;fixtypes;fixctxs;fiximps} = + List.map4 (fun name typ ctx impargs -> let args = List.map Context.Rel.Declaration.get_name ctx in Declare.CInfo.make ~name ~typ ~args ~impargs () - ) fixnames fixtypes fiximps - -let declare_recursive ~fix_kind ~possible_guard ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = - let cinfo = build_recthms fixnames fixtypes fiximps in - let kind = Decls.IsDefinition fix_kind in - let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ?typing_flags ?user_warns ~ntns () in - match Option.List.map (fun x -> x) fixdefs with - | Some fixdefs -> - (* All bodies are defined *) - let _ : GlobRef.t list = - Declare.declare_mutual_definitions ~cinfo ~info ~opaque:false ~uctx - ~possible_guard ~bodies:(fixdefs,fixrs) ?using () + ) fixnames fixtypes fixctxs fiximps + +let collect_evars_of_term evd c ty = + Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) + +let out_def = function + | Some def -> def + | None -> CErrors.user_err Pp.(str "Program Fixpoint needs defined bodies.") + +let collect_evars env sigma rec_sign name def typ = + (* Generalize by the recursive prototypes *) + let deps = collect_evars_of_term sigma def typ in + let evars, _, def, typ = + RetrieveObl.retrieve_obligations env name sigma + (List.length rec_sign) ~deps def typ in + (Some def, typ, evars) + +let finish_program env sigma rec_sign possible_guard {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns} = + (* Get the interesting evars, those that were not instantiated *) + let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env sigma in + (* Solve remaining evars *) + let sigma = Evarutil.nf_evar_map_undefined sigma in + let fixdefs = List.map out_def fixdefs in + (* An early check of guardedness before working on the obligations *) + let () = + let fixdecls = + Array.of_list (List.map2 (fun x r -> Context.make_annot (Name x) r) fixnames fixrs), + Array.of_list fixtypes, + Array.of_list fixdefs in - None + ignore (Pretyping.esearch_guard env sigma possible_guard fixdecls) in + let fixdefs, fixtypes, obls = List.split3 (List.map3 (collect_evars env sigma rec_sign) fixnames fixdefs fixtypes) in + let fixrs = List.map (EConstr.ERelevance.kind sigma) fixrs in + sigma, {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns}, obls + +let finish_regular env sigma fix = + let sigma = Pretyping.(solve_remaining_evars all_no_fail_flags env sigma) in + sigma, ground_fixpoint env sigma fix, [] + +let do_mutually_recursive ?pm ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using (rec_order, fixl) + : Declare.OblState.t option * Declare.Proof.t option = + let env = Global.env () in + let env = Environ.update_typing_flags ?typing_flags env in + let (env,rec_sign,sigma),(fix,isfix,possible_guard,udecl) = interp_recursive_evars env ~program_mode:(Option.has_some pm) (true, rec_order) fixl in + check_recursive ~isfix env sigma fix; + let kind = Decls.IsDefinition isfix in + let sigma, ({fixdefs=bodies;fixrs} as fix), obls = + match pm with + | Some pm -> finish_program env sigma rec_sign possible_guard fix + | None -> finish_regular env sigma fix in + let uctx = Evd.evar_universe_context sigma in + let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ?typing_flags ?user_warns ~ntns:fix.fixntns () in + let cinfo = build_recthms fix in + match pm with + | Some pm -> + let bodies = List.map Option.get bodies in + Some (Declare.Obls.add_mutual_definitions ~pm ~cinfo ~info ~opaque:false ~uctx ~bodies ~possible_guard ?using obls), None | None -> - (* At least one undefined body *) - let evd = Evd.from_ctx uctx in - let lemma = Declare.Proof.start_mutual_definitions ~info ~cinfo - ~bodies:fixdefs ~possible_guard ?using evd in - Some lemma - -let do_mutually_recursive ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using (rec_order, fixl) : Declare.Proof.t option = - let ntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in - let fix_kind, possible_guard, fix = interp_recursive ?typing_flags (true, rec_order) fixl in - declare_recursive ~fix_kind ~possible_guard ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using fix ntns + try + let bodies = List.map Option.get bodies in + (* All bodies are defined *) + let _ : GlobRef.t list = + Declare.declare_mutual_definitions ~cinfo ~info ~opaque:false ~uctx + ~possible_guard ~bodies:(bodies,fixrs) ?using () + in + None, None + with Option.IsNone -> + (* At least one undefined body *) + let evd = Evd.from_ctx uctx in + let lemma = Declare.Proof.start_mutual_definitions ~info ~cinfo + ~bodies ~possible_guard ?using evd in + None, Some lemma diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 58313b1ec9ca..59e23c02413b 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -16,45 +16,28 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_mutually_recursive - : ?scope:Locality.definition_scope + : ?pm:Declare.OblState.t + -> ?scope:Locality.definition_scope -> ?clearbody:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags -> ?user_warns:UserWarn.t -> ?using:Vernacexpr.section_subset_expr -> recursives_expr - -> Declare.Proof.t option + -> Declare.OblState.t option * Declare.Proof.t option (************************************************************************) (** Internal API *) (************************************************************************) -(** names / relevance / defs / types *) -type ('constr, 'types, 'r) recursive_preentry = Id.t list * 'r list * 'constr option list * 'types list - -(** Exported for Program *) -val interp_recursive_evars : - Environ.env -> - (* Misc arguments *) - program_mode:bool -> - (* Notations of the fixpoint / should that be folded in the previous argument? *) - bool * recursion_order_expr -> - recursive_expr_gen list -> - (* env / signature / univs / evar_map *) - (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * - (* names / defs / types *) - (EConstr.t, EConstr.types, EConstr.ERelevance.t) recursive_preentry * - (* ctx per mutual def / implicits / struct annotations *) - (EConstr.rel_context * Impargs.manual_implicits) list * Decls.definition_object_kind * Pretyping.possible_guard +(** names / relevance / defs / types / contexts / implicit args / struct annotations / universe decl *) +type ('constr, 'types, 'r) recursive_preentry = + (Id.t list * 'r list * 'constr option list * 'types list * EConstr.rel_context list * Impargs.manual_implicits list) * + Decls.definition_object_kind * Pretyping.possible_guard * UState.universe_decl (** Exported for Funind *) -val interp_recursive - : ?check_recursivity:bool - -> ?typing_flags:Declarations.typing_flags - -> bool * Vernacexpr.recursion_order_expr +val interp_fixpoint_short + : Constrexpr.fixpoint_order_expr option list -> recursive_expr_gen list - -> Decls.definition_object_kind * Pretyping.possible_guard * - ((Constr.t, Constr.types, Sorts.relevance) recursive_preentry * - UState.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits) list) + -> Constr.types list * UState.t diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 9fc2cff43e25..567e9234db6f 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -21,7 +21,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Evarutil open Context.Rel.Declaration open ComFixpoint @@ -210,49 +209,10 @@ let out_def = function | Some def -> def | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") -let collect_evars_of_term evd c ty = - Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) - -let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (rec_order, fixl) = - let (env, rec_sign, udecl, evd), fix, info, kind, possible_guard = - let env = Global.env () in - let env = Environ.update_typing_flags ?typing_flags env in - interp_recursive_evars env ~program_mode:true (false, rec_order) fixl - in - (* Program-specific code *) - (* Get the interesting evars, those that were not instantiated *) - let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in - (* Solve remaining evars *) - let evd = nf_evar_map_undefined evd in - let (fixnames,fixrs,fixdefs,fixtypes) = fix in - let collect_evars name def typ impargs = - (* Generalize by the recursive prototypes *) - let def = nf_evar evd def in - let typ = nf_evar evd typ in - let deps = collect_evars_of_term evd def typ in - let evars, _, def, typ = - RetrieveObl.retrieve_obligations env name evd - (List.length rec_sign) ~deps def typ in - (def, evars, typ) - in - let fiximps = List.map snd info in - let fixdefs = List.map out_def fixdefs in - let bodies, obls, typs = List.split3 (List.map4 collect_evars fixnames fixdefs fixtypes fiximps) in - let cinfo = List.map3 (fun name typ impargs -> Declare.CInfo.make ~name ~typ ~impargs ()) fixnames typs fiximps in - let () = - (* An early check of guardedness before working on the obligations *) - let fixdecls = - Array.of_list (List.map2 (fun x r -> make_annot (Name x) r) fixnames fixrs), - Array.of_list fixtypes, - Array.of_list fixdefs - in - ignore (Pretyping.esearch_guard env evd possible_guard fixdecls) - in - let uctx = Evd.evar_universe_context evd in - let kind = Decls.(IsDefinition kind) in - let ntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in - let info = Declare.Info.make ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns ~ntns () in - Declare.Obls.add_mutual_definitions ~pm ~info ~cinfo ~opaque:false ~uctx ~bodies ~possible_guard ?using obls +let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fixl = + let pm, proof = do_mutually_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fixl in + assert (Option.is_empty proof); + Option.get pm let do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (fix_order, l) = match fix_order, l with diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d9803141cddb..a4b03dc1c0e8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1101,7 +1101,9 @@ let vernac_fixpoint ~atts ~pm (rec_order,fixl as fix) = let pm = ComProgramFixpoint.do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fix in Some pm, None else - let proof = ComFixpoint.do_mutually_recursive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (CFixRecOrder rec_order, fixl) in + let pm', proof = + ComFixpoint.do_mutually_recursive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (CFixRecOrder rec_order, fixl) in + assert (Option.is_empty pm'); pm, proof let vernac_cofixpoint_common ~atts l = @@ -1125,7 +1127,9 @@ let vernac_cofixpoint ~atts ~pm l = let pm = ComProgramFixpoint.do_cofixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l in Some pm, None else - let proof = ComFixpoint.do_mutually_recursive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (CCoFixRecOrder, l) in + let pm', proof = + ComFixpoint.do_mutually_recursive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (CCoFixRecOrder, l) in + assert (Option.is_empty pm'); pm, proof let vernac_scheme l =