aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml8
-rw-r--r--vernac/comDefinition.ml2
-rw-r--r--vernac/declare.ml47
-rw-r--r--vernac/declare.mli24
-rw-r--r--vernac/obligations.ml54
-rw-r--r--vernac/topfmt.ml3
6 files changed, 63 insertions, 75 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5323c9f1c6..bb640a83f6 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -385,7 +385,7 @@ let build_beq_scheme mode kn =
Vars.substl subst cores.(i)
in
create_input fix),
- UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()))
+ UState.from_env (Global.env ()))
let beq_scheme_kind =
declare_mutual_scheme_object "_beq"
@@ -707,7 +707,7 @@ let make_bl_scheme mode mind =
let lnonparrec,lnamesparrec = (* TODO subst *)
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let bl_goal = compute_bl_goal ind lnamesparrec nparrec in
- let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+ let uctx = UState.from_env (Global.env ()) in
let side_eff = side_effect_of_mode mode in
let bl_goal = EConstr.of_constr bl_goal in
let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
@@ -840,7 +840,7 @@ let make_lb_scheme mode mind =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let lb_goal = compute_lb_goal ind lnamesparrec nparrec in
- let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+ let uctx = UState.from_env (Global.env ()) in
let side_eff = side_effect_of_mode mode in
let lb_goal = EConstr.of_constr lb_goal in
let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
@@ -1010,7 +1010,7 @@ let make_eq_decidability mode mind =
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
let u = Univ.Instance.empty in
- let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+ let uctx = UState.from_env (Global.env ()) in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let side_eff = side_effect_of_mode mode in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index eac8f92e2e..d56917271c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
let (body, types), evd, udecl, impargs =
interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
in
- let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
+ let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in
let _ : Declare.Obls.progress =
Obligations.add_definition
~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c291890dce..c77d4909da 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1007,25 +1007,20 @@ let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
-let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
+let prepare_obligation ~name ~types ~body sigma =
+ let env = Global.env () in
+ let types = match types with
+ | Some t -> t
+ | None -> Retyping.get_type_of env sigma body
+ in
let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
- sigma (fun nf -> nf body, Option.map nf types)
+ sigma (fun nf -> nf body, nf types)
in
- let univs = Evd.check_univ_decl ~poly sigma udecl in
- let ce = definition_entry ?opaque ?inline ?types ~univs body in
- let env = Global.env () in
- let (c,ctx), sideff = Future.force ce.proof_entry_body in
- assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private);
- assert(Univ.ContextSet.is_empty ctx);
RetrieveObl.check_evars env sigma;
- let c = EConstr.of_constr c in
- let typ = match ce.proof_entry_type with
- | Some t -> EConstr.of_constr t
- | None -> Retyping.get_type_of env sigma c
- in
- let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in
+ let body, types = EConstr.(of_constr body, of_constr types) in
+ let obls, _, body, cty = RetrieveObl.retrieve_obligations env name sigma 0 body types in
let uctx = Evd.evar_universe_context sigma in
- c, cty, uctx, obls
+ body, cty, uctx, obls
let prepare_parameter ~poly ~udecl ~types sigma =
let env = Global.env () in
@@ -1215,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
@@ -1239,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 _ ->
@@ -1626,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 *)
@@ -1641,7 +1636,7 @@ let obligation_terminator entries uctx {name; num; auto} =
universes and constraints if any *)
defined
then
- UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
+ UState.from_env (Global.env ())
else uctx
in
update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
@@ -1673,9 +1668,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
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.from_env (Global.env ()) in
let ctx' = UState.merge_subst ctx (UState.subst ctx') in
(Univ.Instance.empty, ctx')
else
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 82b0cff8d9..647896e2f5 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -367,11 +367,7 @@ val declare_mutually_recursive
(** Prepare API, to be removed once we provide the corresponding 1-step API *)
val prepare_obligation
- : ?opaque:bool
- -> ?inline:bool
- -> name:Id.t
- -> poly:bool
- -> udecl:UState.universe_decl
+ : name:Id.t
-> types:EConstr.t option
-> body:EConstr.t
-> Evd.evar_map
@@ -443,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
@@ -521,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 5fdee9f2d4..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,18 +182,16 @@ 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 evd = Evd.from_env (Global.env ()) in
- let evd = Evd.merge_universe_subst evd (UState.subst ctx) in
- let ctx' = Evd.evar_universe_context evd in
- Some (ProgramDecl.set_uctx ~uctx:ctx' prg))
+ 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
@@ -254,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 =
@@ -373,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;
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 2d8734ff7f..a28d8f605b 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -404,6 +404,7 @@ let with_output_to_file fname func input =
let channel = open_out (String.concat "." [fname; "out"]) in
let old_fmt = !std_ft, !err_ft, !deep_ft in
let new_ft = Format.formatter_of_out_channel channel in
+ set_gp new_ft (get_gp !std_ft);
std_ft := new_ft;
err_ft := new_ft;
deep_ft := new_ft;
@@ -412,6 +413,7 @@ let with_output_to_file fname func input =
std_ft := Util.pi1 old_fmt;
err_ft := Util.pi2 old_fmt;
deep_ft := Util.pi3 old_fmt;
+ Format.pp_print_flush new_ft ();
close_out channel;
output
with reraise ->
@@ -419,6 +421,7 @@ let with_output_to_file fname func input =
std_ft := Util.pi1 old_fmt;
err_ft := Util.pi2 old_fmt;
deep_ft := Util.pi3 old_fmt;
+ Format.pp_print_flush new_ft ();
close_out channel;
Exninfo.iraise reraise
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 13:00:28 +0000