aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--stm/stm.ml2
-rw-r--r--vernac/declareObl.ml155
-rw-r--r--vernac/declareObl.mli133
-rw-r--r--vernac/obligations.ml132
4 files changed, 242 insertions, 180 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 73356c42f1..62556d38ff 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -878,7 +878,7 @@ end = struct (* {{{ *)
Vernacstate.LemmaStack.t option *
int * (* Evarutil.meta_counter_summary_tag *)
int * (* Evd.evar_counter_summary_tag *)
- DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+ DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
type partial_state =
[ `Full of Vernacstate.t
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 8b0666aab7..df39f7be4b 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -18,39 +18,94 @@ open Entries
type 'a obligation_body = DefinedObl of 'a | TermObl of constr
-type obligation =
- { obl_name : Id.t
- ; obl_type : types
- ; obl_location : Evar_kinds.t Loc.located
- ; obl_body : pconstant obligation_body option
- ; obl_status : bool * Evar_kinds.obligation_definition_status
- ; obl_deps : Int.Set.t
- ; obl_tac : unit Proofview.tactic option }
+module Obligation = struct
+ type t =
+ { obl_name : Id.t
+ ; obl_type : types
+ ; obl_location : Evar_kinds.t Loc.located
+ ; obl_body : pconstant obligation_body option
+ ; obl_status : bool * Evar_kinds.obligation_definition_status
+ ; obl_deps : Int.Set.t
+ ; obl_tac : unit Proofview.tactic option }
-type obligations = obligation array * int
+ let set_type ~typ obl = { obl with obl_type = typ }
+ let set_body ~body obl = { obl with obl_body = Some body }
+
+end
+
+type obligations = Obligation.t array * int
type fixpoint_kind =
| IsFixpoint of lident option list
| IsCoFixpoint
-type program_info =
- { prg_name : Id.t
- ; prg_body : constr
- ; prg_type : constr
- ; prg_ctx : UState.t
- ; prg_univdecl : UState.universe_decl
- ; prg_obligations : obligations
- ; prg_deps : Id.t list
- ; prg_fixkind : fixpoint_kind option
- ; prg_implicits : Impargs.manual_implicits
- ; prg_notations : Vernacexpr.decl_notation list
- ; prg_poly : bool
- ; prg_scope : DeclareDef.locality
- ; prg_kind : Decls.definition_object_kind
- ; prg_reduce : constr -> constr
- ; prg_hook : DeclareDef.Hook.t option
- ; prg_opaque : bool
- }
+module ProgramDecl = struct
+
+ type t =
+ { prg_name : Id.t
+ ; prg_body : constr
+ ; prg_type : constr
+ ; prg_ctx : UState.t
+ ; prg_univdecl : UState.universe_decl
+ ; prg_obligations : obligations
+ ; prg_deps : Id.t list
+ ; prg_fixkind : fixpoint_kind option
+ ; prg_implicits : Impargs.manual_implicits
+ ; prg_notations : Vernacexpr.decl_notation list
+ ; prg_poly : bool
+ ; prg_scope : DeclareDef.locality
+ ; prg_kind : Decls.definition_object_kind
+ ; prg_reduce : constr -> constr
+ ; prg_hook : DeclareDef.Hook.t option
+ ; prg_opaque : bool
+ }
+
+ open Obligation
+
+ let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs
+ ~poly ~scope ~kind b t deps fixkind notations obls reduce =
+ let obls', b =
+ match b with
+ | None ->
+ assert(Int.equal (Array.length obls) 0);
+ let n = Nameops.add_suffix n "_obligation" in
+ [| { obl_name = n; obl_body = None;
+ obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t;
+ obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
+ obl_tac = None } |],
+ mkVar n
+ | Some b ->
+ Array.mapi
+ (fun i (n, t, l, o, d, tac) ->
+ { obl_name = n ; obl_body = None;
+ obl_location = l; obl_type = t; obl_status = o;
+ obl_deps = d; obl_tac = tac })
+ obls, b
+ in
+ let ctx = UState.make_flexible_nonalgebraic uctx in
+ { prg_name = n
+ ; prg_body = b
+ ; prg_type = reduce t
+ ; prg_ctx = ctx
+ ; prg_univdecl = udecl
+ ; prg_obligations = (obls', Array.length obls')
+ ; prg_deps = deps
+ ; prg_fixkind = fixkind
+ ; prg_notations = notations
+ ; prg_implicits = impargs
+ ; prg_poly = poly
+ ; prg_scope = scope
+ ; prg_kind = kind
+ ; prg_reduce = reduce
+ ; prg_hook = hook
+ ; prg_opaque = opaque
+ }
+
+ let set_uctx ~uctx prg = {prg with prg_ctx = uctx}
+end
+
+open Obligation
+open ProgramDecl
(* Saving an obligation *)
@@ -120,16 +175,16 @@ let shrink_body c ty =
in
(ctx, b', ty', Array.of_list args)
+(***********************************************************************)
+(* Saving an obligation *)
+(***********************************************************************)
+
let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
let add_hint local prg cst =
let locality = if local then Goptions.OptLocal else Goptions.OptExport in
Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst)
-(***********************************************************************)
-(* Saving an obligation *)
-(***********************************************************************)
-
(* true = hide obligations *)
let get_hide_obligations =
Goptions.declare_bool_option_and_ref
@@ -205,7 +260,7 @@ let close sec =
++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ")
++ str "unsolved obligations" ))
-let input : program_info CEphemeron.key ProgMap.t -> Libobject.obj =
+let input : ProgramDecl.t CEphemeron.key ProgMap.t -> Libobject.obj =
let open Libobject in
declare_object
{ (default_object "Program state") with
@@ -543,3 +598,39 @@ let obligation_terminator entries uctx { name; num; auto } =
str
"[obligation_terminator] close_proof returned more than one proof \
term")
+
+(* Similar to the terminator but for interactive paths, as the
+ terminator is only called in interactive proof mode *)
+let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } =
+ let obls, rem = prg.prg_obligations in
+ let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in
+ let transparent = evaluable_constant cst (Global.env ()) in
+ let () = match obl.obl_status with
+ (true, Evar_kinds.Expand)
+ | (true, Evar_kinds.Define true) ->
+ if not transparent then err_not_transp ()
+ | _ -> ()
+ in
+ let inst, ctx' =
+ if not prg.prg_poly (* Not polymorphic *) then
+ (* The universe context was declared globally, we continue
+ from the new global environment. *)
+ let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+ let ctx' = UState.merge_subst ctx (UState.subst ctx') in
+ Univ.Instance.empty, ctx'
+ else
+ (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
+ let uctx = UState.context ctx' in
+ Univ.UContext.instance uctx, ctx'
+ in
+ let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
+ let () = if transparent then add_hint true prg cst in
+ let obls = Array.copy obls in
+ let () = obls.(num) <- obl in
+ let prg = { prg with prg_ctx = ctx' } in
+ let () = ignore (update_obls prg obls (pred rem)) in
+ if pred rem > 0 then begin
+ let deps = dependencies obls num in
+ if not (Int.Set.is_empty deps) then
+ ignore (auto (Some prg.prg_name) deps None)
+ end
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 6e7700a28a..c2bd0595fa 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -13,61 +13,99 @@ open Constr
type 'a obligation_body = DefinedObl of 'a | TermObl of constr
-type obligation =
- { obl_name : Id.t
- ; obl_type : types
- ; obl_location : Evar_kinds.t Loc.located
- ; obl_body : pconstant obligation_body option
- ; obl_status : bool * Evar_kinds.obligation_definition_status
- ; obl_deps : Int.Set.t
- ; obl_tac : unit Proofview.tactic option }
+module Obligation : sig
-type obligations = obligation array * int
+ type t = private
+ { obl_name : Id.t
+ ; obl_type : types
+ ; obl_location : Evar_kinds.t Loc.located
+ ; obl_body : pconstant obligation_body option
+ ; obl_status : bool * Evar_kinds.obligation_definition_status
+ ; obl_deps : Int.Set.t
+ ; obl_tac : unit Proofview.tactic option }
+
+ val set_type : typ:Constr.types -> t -> t
+ val set_body : body:pconstant obligation_body -> t -> t
+
+end
+
+type obligations = Obligation.t array * int
type fixpoint_kind =
| IsFixpoint of lident option list
| IsCoFixpoint
-type program_info =
- { prg_name : Id.t
- ; prg_body : constr
- ; prg_type : constr
- ; prg_ctx : UState.t
- ; prg_univdecl : UState.universe_decl
- ; prg_obligations : obligations
- ; prg_deps : Id.t list
- ; prg_fixkind : fixpoint_kind option
- ; prg_implicits : Impargs.manual_implicits
- ; prg_notations : Vernacexpr.decl_notation list
- ; prg_poly : bool
- ; prg_scope : DeclareDef.locality
- ; prg_kind : Decls.definition_object_kind
- ; prg_reduce : constr -> constr
- ; prg_hook : DeclareDef.Hook.t option
- ; prg_opaque : bool
- }
+(* Information about a single [Program {Definition,Lemma,..}] declaration *)
+module ProgramDecl : sig
+
+ type t = private
+ { prg_name : Id.t
+ ; prg_body : constr
+ ; prg_type : constr
+ ; prg_ctx : UState.t
+ ; prg_univdecl : UState.universe_decl
+ ; prg_obligations : obligations
+ ; prg_deps : Id.t list
+ ; prg_fixkind : fixpoint_kind option
+ ; prg_implicits : Impargs.manual_implicits
+ ; prg_notations : Vernacexpr.decl_notation list
+ ; prg_poly : bool
+ ; prg_scope : DeclareDef.locality
+ ; prg_kind : Decls.definition_object_kind
+ ; prg_reduce : constr -> constr
+ ; prg_hook : DeclareDef.Hook.t option
+ ; prg_opaque : bool
+ }
+
+ val make :
+ ?opaque:bool
+ -> ?hook:DeclareDef.Hook.t
+ -> Names.Id.t
+ -> udecl:UState.universe_decl
+ -> uctx:UState.t
+ -> impargs:Impargs.manual_implicits
+ -> poly:bool
+ -> scope:DeclareDef.locality
+ -> kind:Decls.definition_object_kind
+ -> Constr.constr option
+ -> Constr.types
+ -> Names.Id.t list
+ -> fixpoint_kind option
+ -> Vernacexpr.decl_notation list
+ -> ( Names.Id.t
+ * Constr.types
+ * Evar_kinds.t Loc.located
+ * (bool * Evar_kinds.obligation_definition_status)
+ * Int.Set.t
+ * unit Proofview.tactic option )
+ array
+ -> (Constr.constr -> Constr.constr)
+ -> t
+
+ val set_uctx : uctx:UState.t -> t -> t
+end
val declare_obligation :
- program_info
- -> obligation
+ ProgramDecl.t
+ -> Obligation.t
-> Constr.types
-> Constr.types option
-> Entries.universes_entry
- -> bool * obligation
+ -> bool * Obligation.t
(** [declare_obligation] Save an obligation *)
module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set
-val declare_definition : program_info -> Names.GlobRef.t
+val declare_definition : ProgramDecl.t -> Names.GlobRef.t
+(** Resolution status of a program *)
type progress =
- (* Resolution status of a program *)
| Remain of int
- (* n obligations remaining *)
+ (** n obligations remaining *)
| Dependent
- (* Dependent on other definitions *)
+ (** Dependent on other definitions *)
| Defined of GlobRef.t
- (* Defined as id *)
+ (** Defined as id *)
type obligation_qed_info =
{ name : Id.t
@@ -79,32 +117,41 @@ val obligation_terminator
: Evd.side_effects Declare.proof_entry list
-> UState.t
-> obligation_qed_info -> unit
-(** [obligation_terminator] part 2 of saving an obligation *)
+(** [obligation_terminator] part 2 of saving an obligation, proof mode *)
+
+val obligation_hook
+ : ProgramDecl.t
+ -> Obligation.t
+ -> Int.t
+ -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b)
+ -> DeclareDef.Hook.S.t
+ -> unit
+(** [obligation_hook] part 2 of saving an obligation, non-interactive mode *)
val update_obls :
- program_info
- -> obligation array
+ ProgramDecl.t
+ -> Obligation.t array
-> int
-> progress
(** [update_obls prg obls n progress] What does this do? *)
(** { 2 Util } *)
-val get_prg_info_map : unit -> program_info CEphemeron.key ProgMap.t
+val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t
val program_tcc_summary_tag :
- program_info CEphemeron.key Id.Map.t Summary.Dyn.tag
+ ProgramDecl.t CEphemeron.key Id.Map.t Summary.Dyn.tag
val obl_substitution :
bool
- -> obligation array
+ -> Obligation.t array
-> Int.Set.t
-> (ProgMap.key * (Constr.types * Constr.types)) list
-val dependencies : obligation array -> int -> Int.Set.t
+val dependencies : Obligation.t array -> int -> Int.Set.t
val err_not_transp : unit -> unit
-val progmap_add : ProgMap.key -> program_info CEphemeron.key -> unit
+val progmap_add : ProgMap.key -> ProgramDecl.t CEphemeron.key -> unit
(* This is a hack to make it possible for Obligations to craft a Qed
* behind the scenes. The fix_exn the Stm attaches to the Future proof
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 9418231cf5..a9d43e851d 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -28,7 +28,10 @@ open Util
module NamedDecl = Context.Named.Declaration
+(* For the records fields, opens should go away one these types are private *)
open DeclareObl
+open DeclareObl.Obligation
+open DeclareObl.ProgramDecl
let succfix (depth, fixrels) =
(succ depth, List.map succ fixrels)
@@ -189,8 +192,6 @@ let sort_dependencies evl =
| [] -> List.rev list
in aux evl Evar.Set.empty []
-open Environ
-
let eterm_obligations env name evm fs ?status t ty =
(* 'Serialize' the evars *)
let nc = Environ.named_context env in
@@ -284,66 +285,22 @@ let default_tactic = ref (Proofview.tclUNIT ())
let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
let subst_deps expand obls deps t =
- let osubst = obl_substitution expand obls deps in
+ let osubst = DeclareObl.obl_substitution expand obls deps in
(Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
let subst_deps_obl obls obl =
let t' = subst_deps true obls obl.obl_deps obl.obl_type in
- { obl with obl_type = t' }
+ Obligation.set_type ~typ:t' obl
open Evd
-let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
-
-let add_local_hint prg cst =
- Hints.add_hints ~locality:Goptions.OptLocal [Id.to_string prg.prg_name] (unfold_entry cst)
-
-let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind
- notations obls impls ~scope ~poly ~kind reduce =
- let obls', b =
- match b with
- | None ->
- assert(Int.equal (Array.length obls) 0);
- let n = Nameops.add_suffix n "_obligation" in
- [| { obl_name = n; obl_body = None;
- obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t;
- obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
- obl_tac = None } |],
- mkVar n
- | Some b ->
- Array.mapi
- (fun i (n, t, l, o, d, tac) ->
- { obl_name = n ; obl_body = None;
- obl_location = l; obl_type = t; obl_status = o;
- obl_deps = d; obl_tac = tac })
- obls, b
- in
- let ctx = UState.make_flexible_nonalgebraic ctx in
- { prg_name = n
- ; prg_body = b
- ; prg_type = reduce t
- ; prg_ctx = ctx
- ; prg_univdecl = udecl
- ; prg_obligations = (obls', Array.length obls')
- ; prg_deps = deps
- ; prg_fixkind = fixkind
- ; prg_notations = notations
- ; prg_implicits = impls
- ; prg_poly = poly
- ; prg_scope = scope
- ; prg_kind = kind
- ; prg_reduce = reduce
- ; prg_hook = hook
- ; prg_opaque = opaque
- }
-
let map_cardinal m =
let i = ref 0 in
ProgMap.iter (fun _ v ->
if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m;
!i
-exception Found of program_info CEphemeron.key
+exception Found of ProgramDecl.t CEphemeron.key
let map_first m =
try
@@ -436,40 +393,6 @@ let solve_by_tac ?loc name evi t poly uctx =
warn_solve_errored ?loc err;
None
-let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } =
- let obls, rem = prg.prg_obligations in
- let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in
- let transparent = evaluable_constant cst (Global.env ()) in
- let () = match obl.obl_status with
- (true, Evar_kinds.Expand)
- | (true, Evar_kinds.Define true) ->
- if not transparent then err_not_transp ()
- | _ -> ()
- in
- let inst, ctx' =
- if not prg.prg_poly (* Not polymorphic *) then
- (* The universe context was declared globally, we continue
- from the new global environment. *)
- let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
- let ctx' = UState.merge_subst ctx (UState.subst ctx') in
- Univ.Instance.empty, ctx'
- else
- (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
- let uctx = UState.context ctx' in
- Univ.UContext.instance uctx, ctx'
- in
- let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
- let () = if transparent then add_local_hint prg cst in
- let obls = Array.copy obls in
- let () = obls.(num) <- obl in
- let prg = { prg with prg_ctx = ctx' } in
- let () = ignore (update_obls prg obls (pred rem)) in
- if pred rem > 0 then begin
- let deps = dependencies obls num in
- if not (Int.Set.is_empty deps) then
- ignore (auto (Some prg.prg_name) deps None)
- end
-
let rec solve_obligation prg num tac =
let user_num = succ num in
let obls, rem = prg.prg_obligations in
@@ -489,7 +412,7 @@ let rec solve_obligation prg num tac =
let evd = Evd.update_sigma_env evd (Global.env ()) in
let auto n oblset tac = auto_solve_obligations n ~oblset tac in
let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in
- let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in
+ let hook = DeclareDef.Hook.make (DeclareObl.obligation_hook prg obl num auto) in
let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in
let poly = prg.prg_poly in
let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in
@@ -530,8 +453,9 @@ and solve_obligation_by_tac prg obls i tac =
prg.prg_poly (Evd.evar_universe_context evd) with
| None -> None
| Some (t, ty, ctx) ->
+ let prg = ProgramDecl.set_uctx ~uctx:ctx prg in
+ (* Why is uctx not used above? *)
let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in
- let prg = {prg with prg_ctx = ctx} in
let def, obl' = declare_obligation prg obl t ty uctx in
obls.(i) <- obl';
if def && not prg.prg_poly then (
@@ -539,7 +463,7 @@ and solve_obligation_by_tac prg obls i tac =
let evd = Evd.from_env (Global.env ()) in
let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
let ctx' = Evd.evar_universe_context evd in
- Some {prg with prg_ctx = ctx'})
+ Some (ProgramDecl.set_uctx ~uctx:ctx' prg))
else Some prg
else None
@@ -553,20 +477,20 @@ and solve_prg_obligations prg ?oblset tac =
| Some s -> set := s;
(fun i -> Int.Set.mem i !set)
in
- let prgref = ref prg in
- let () =
- Array.iteri (fun i x ->
+ let prg =
+ Array.fold_left_i (fun i prg x ->
if p i then
- match solve_obligation_by_tac !prgref obls' i tac with
- | None -> ()
- | Some prg' ->
- prgref := prg';
- let deps = dependencies obls i in
- (set := Int.Set.union !set deps;
- decr rem))
- obls'
+ match solve_obligation_by_tac prg obls' i tac with
+ | None -> prg
+ | Some prg ->
+ let deps = dependencies obls i in
+ set := Int.Set.union !set deps;
+ decr rem;
+ prg
+ else prg)
+ prg obls'
in
- update_obls !prgref obls' !rem
+ update_obls prg obls' !rem
and solve_obligations n tac =
let prg = get_prog_err n in
@@ -632,7 +556,7 @@ let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl)
?(impargs=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
?(reduce=reduce) ?hook ?(opaque = false) obls =
let info = Id.print name ++ str " has type-checked" in
- let prg = init_prog_info ~opaque name udecl term t uctx [] None [] obls impargs ~poly ~scope ~kind reduce ?hook in
+ let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -652,9 +576,9 @@ let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic
?hook ?(opaque = false) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
- (fun (n, b, t, imps, obls) ->
- let prg = init_prog_info ~opaque n udecl (Some b) t uctx deps (Some fixkind)
- notations obls imps ~poly ~scope ~kind reduce ?hook
+ (fun (n, b, t, impargs, obls) ->
+ let prg = ProgramDecl.make ~opaque n ~udecl (Some b) t ~uctx deps (Some fixkind)
+ notations obls ~impargs ~poly ~scope ~kind reduce ?hook
in progmap_add n (CEphemeron.create prg)) l;
let _defined =
List.fold_left (fun finished x ->
@@ -682,10 +606,10 @@ let admit_prog prg =
(Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural)
in
assumption_message x.obl_name;
- obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
+ obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
| Some _ -> ())
obls;
- ignore(update_obls prg obls 0)
+ ignore(DeclareObl.update_obls prg obls 0)
let rec admit_all_obligations () =
let prg = try Some (get_any_prog ()) with NoObligations _ -> None in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 00:46:32 +0000