diff options
| -rw-r--r-- | vernac/declare.ml | 16 | ||||
| -rw-r--r-- | vernac/declare.mli | 18 | ||||
| -rw-r--r-- | vernac/obligations.ml | 51 |
3 files changed, 41 insertions, 44 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 333b186b22..c77d4909da 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1210,19 +1210,20 @@ let get_hide_obligations = ~key:["Hide"; "Obligations"] ~value:false -let declare_obligation prg obl body ty uctx = +let declare_obligation prg obl ~uctx ~types ~body = + let univs = UState.univ_entry ~poly:prg.prg_poly uctx in let body = prg.prg_reduce body in - let ty = Option.map prg.prg_reduce ty in + let types = Option.map prg.prg_reduce types in match obl.obl_status with | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) | force, Evar_kinds.Define opaque -> let opaque = (not force) && opaque in let poly = prg.prg_poly in let ctx, body, ty, args = - if not poly then shrink_body body ty - else ([], body, ty, [||]) + if not poly then shrink_body body types + else ([], body, types, [||]) in - let ce = definition_entry ?types:ty ~opaque ~univs:uctx body in + let ce = definition_entry ?types:ty ~opaque ~univs body in (* ppedrot: seems legit to have obligations as local *) let constant = declare_constant ~name:obl.obl_name @@ -1234,7 +1235,7 @@ let declare_obligation prg obl body ty uctx = add_hint (Locality.make_section_locality None) prg constant; definition_message obl.obl_name; let body = - match uctx with + match univs with | Entries.Polymorphic_entry (_, uctx) -> Some (DefinedObl (constant, Univ.UContext.instance uctx)) | Entries.Monomorphic_entry _ -> @@ -1621,8 +1622,7 @@ let obligation_terminator entries uctx {name; num; auto} = in let obl = {obl with obl_status = (false, status)} in let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in - let univs = UState.univ_entry ~poly:prg.prg_poly uctx in - let defined, obl = declare_obligation prg obl body ty univs in + let defined, obl = declare_obligation prg obl ~body ~types:ty ~uctx in let prg_ctx = if prg.prg_poly then (* Polymorphic *) diff --git a/vernac/declare.mli b/vernac/declare.mli index 62bc6a34bf..647896e2f5 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -439,26 +439,21 @@ module ProgramDecl : sig -> 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 + -> RetrieveObl.obligation_info -> (Constr.constr -> Constr.constr) -> t val set_uctx : uctx:UState.t -> t -> t end -(** [declare_obligation] Save an obligation *) +(** [declare_obligation prg obl ~uctx ~types ~body] Save an obligation + [obl] for program definition [prg] *) val declare_obligation : ProgramDecl.t -> Obligation.t - -> Constr.types - -> Constr.types option - -> Entries.universes_entry + -> uctx:UState.t + -> types:Constr.types option + -> body:Constr.types -> bool * Obligation.t module State : sig @@ -517,7 +512,6 @@ val obl_substitution : -> (Id.t * (Constr.types * Constr.types)) list val dependencies : Obligation.t array -> int -> Int.Set.t -val err_not_transp : unit -> 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 bbc20d5e30..a8eac8fd2d 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -53,7 +53,6 @@ module Error = struct end -let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) @@ -183,16 +182,15 @@ and solve_obligation_by_tac prg obls i tac = match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) 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 + | Some (t, ty, uctx) -> + let prg = ProgramDecl.set_uctx ~uctx prg in (* Why is uctx not used above? *) - let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in - let def, obl' = declare_obligation prg obl t ty uctx in + let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in obls.(i) <- obl'; if def && not prg.prg_poly then ( (* Declare the term constraints with the first obligation only *) - let uctx = UState.from_env (Global.env ()) in - let uctx = UState.merge_subst uctx (UState.subst ctx) in + let uctx_global = UState.from_env (Global.env ()) in + let uctx = UState.merge_subst uctx_global (UState.subst uctx) in Some (ProgramDecl.set_uctx ~uctx prg)) else Some prg else None @@ -253,27 +251,32 @@ and auto_solve_obligations n ?oblset tac : progress = open Pp +let show_single_obligation i n obls x = + let x = subst_deps_obl obls x in + let env = Global.env () in + let sigma = Evd.from_env env in + let msg = + str "Obligation" ++ spc () + ++ int (succ i) + ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc () + ++ hov 1 (Printer.pr_constr_env env sigma x.obl_type + ++ str "." ++ fnl ()) in + Feedback.msg_info msg + let show_obligations_of_prg ?(msg = true) prg = let n = prg.prg_name in let {obls; remaining} = prg.prg_obligations in let showed = ref 5 in if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: "); - Array.iteri (fun i x -> - match x.obl_body with - | None -> - if !showed > 0 then ( - decr showed; - let x = subst_deps_obl obls x in - let env = Global.env () in - let sigma = Evd.from_env env in - Feedback.msg_info - ( str "Obligation" ++ spc () - ++ int (succ i) - ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc () - ++ hov 1 - ( Printer.pr_constr_env env sigma x.obl_type - ++ str "." ++ fnl () ) ) ) - | Some _ -> ()) + Array.iteri + (fun i x -> + match x.obl_body with + | None -> + if !showed > 0 then begin + decr showed; + show_single_obligation i n obls x + end + | Some _ -> ()) obls let show_obligations ?(msg = true) n = @@ -372,7 +375,7 @@ let admit_prog prg = let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified (Declare.ParameterEntry (None, (x.obl_type, ctx), None)) ~kind:Decls.(IsAssumption Conjectural) in - assumption_message x.obl_name; + Declare.assumption_message x.obl_name; obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x | Some _ -> ()) obls; |