aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/obligations.ml')
-rw-r--r--vernac/obligations.ml72
1 files changed, 40 insertions, 32 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 064e40b9b..1ab24b670 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -209,8 +209,10 @@ let eterm_obligations env name evm fs ?status t ty =
List.fold_right
(fun (id, (n, nstr), ev) l ->
let hyps = Evd.evar_filtered_context ev in
- let hyps = trunc_named_context nc_len hyps in
- let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
+ let hyps = trunc_named_context nc_len hyps in
+ let hyps = EConstr.Unsafe.to_named_context hyps in
+ let concl = EConstr.Unsafe.to_constr ev.evar_concl in
+ let evtyp, deps, transp = etype_of_evar l hyps concl in
let evtyp, hyps, chop =
match chop_product fs evtyp with
| Some t -> t, trunc_named_context fs hyps, fs
@@ -257,14 +259,16 @@ let eterm_obligations env name evm fs ?status t ty =
let tactics_module = ["Program";"Tactics"]
let safe_init_constant md name () =
Coqlib.check_required_library ("Coq"::md);
- Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name)
+ UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name)
let hide_obligation = safe_init_constant tactics_module "obligation"
let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
let error s = pperror (str s)
let reduce c =
- EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c))
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c))
exception NoObligations of Id.t option
@@ -294,17 +298,17 @@ type obligation =
type obligations = (obligation array * int)
type fixpoint_kind =
- | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint
-type notations = (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type program_info_aux = {
prg_name: Id.t;
prg_body: constr;
prg_type: constr;
prg_ctx: UState.t;
- prg_univdecl: Univdecls.universe_decl;
+ prg_univdecl: UState.universe_decl;
prg_obligations: obligations;
prg_deps : Id.t list;
prg_fixkind : fixpoint_kind option ;
@@ -356,7 +360,7 @@ let _ =
optread = get_shrink_obligations;
optwrite = set_shrink_obligations; }
-let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
+let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
let get_obligation_body expand obl =
match obl.obl_body with
@@ -470,7 +474,7 @@ let subst_body expand prg =
let declare_definition prg =
let body, typ = subst_body true prg in
- let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
+ let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
(UState.subst prg.prg_ctx) in
let opaque = prg.prg_opaque in
let fix_exn = Hook.get get_fix_exn () in
@@ -519,8 +523,10 @@ let declare_mutual_definition l =
List.split3
(List.map (fun x ->
let subs, typ = (subst_body true x) in
- let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len (EConstr.of_constr subs)) in
- let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len (EConstr.of_constr typ)) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
+ let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
let term = EConstr.Unsafe.to_constr term in
let typ = EConstr.Unsafe.to_constr typ in
x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
@@ -553,15 +559,14 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let univs = UState.const_univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs)
+ let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
- let kn = match gr with ConstRef kn -> kn | _ -> assert false in
Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
- List.iter progmap_remove l; kn
+ List.iter progmap_remove l; gr
let decompose_lam_prod c ty =
let open Context.Rel.Declaration in
@@ -610,7 +615,7 @@ let shrink_body c ty =
let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
let add_hint local prg cst =
- Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+ Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
let it_mkLambda_or_LetIn_or_clean t ctx =
let open Context.Rel.Declaration in
@@ -742,7 +747,7 @@ let all_programs () =
type progress =
| Remain of int
| Dependent
- | Defined of global_reference
+ | Defined of GlobRef.t
let obligations_message rem =
if rem > 0 then
@@ -768,8 +773,8 @@ let update_obls prg obls rem =
let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
if List.for_all (fun x -> obligations_solved x) progs then
let kn = declare_mutual_definition progs in
- Defined (ConstRef kn)
- else Dependent)
+ Defined kn
+ else Dependent)
let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
@@ -813,10 +818,9 @@ let rec string_of_list sep f = function
let solve_by_tac name evi t poly ctx =
let id = name in
- let concl = EConstr.of_constr evi.evar_concl in
(* spiwack: the status is dropped. *)
let (entry,_,ctx') = Pfedit.build_constant_by_tactic
- id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
+ id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in
let env = Global.env () in
let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
let body, () = Future.force entry.const_entry_body in
@@ -848,12 +852,12 @@ let obligation_terminator name num guard hook auto pf =
let obl = obls.(num) in
let status =
match obl.obl_status, opq with
- | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
- | (true, _), Vernacexpr.Opaque -> err_not_transp ()
- | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
- | (_, Evar_kinds.Define true), Vernacexpr.Transparent ->
+ | (_, Evar_kinds.Expand), Opaque -> err_not_transp ()
+ | (true, _), Opaque -> err_not_transp ()
+ | (false, _), Opaque -> Evar_kinds.Define true
+ | (_, Evar_kinds.Define true), Transparent ->
Evar_kinds.Define false
- | (_, status), Vernacexpr.Transparent -> status
+ | (_, status), Transparent -> status
in
let obl = { obl with obl_status = false, status } in
let ctx =
@@ -890,7 +894,7 @@ let obligation_terminator name num guard hook auto pf =
let obligation_hook prg obl num auto ctx' _ gr =
let obls, rem = prg.prg_obligations in
- let cst = match gr with ConstRef cst -> cst | _ -> assert false in
+ let cst = match gr 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)
@@ -957,7 +961,7 @@ and obligation (user_num, name, typ) tac =
let num = pred user_num in
let prg = get_prog_err name in
let obls, rem = prg.prg_obligations in
- if num < Array.length obls then
+ if num >= 0 && num < Array.length obls then
let obl = obls.(num) in
match obl.obl_body with
None -> solve_obligation prg num tac
@@ -1068,9 +1072,11 @@ let show_obligations_of_prg ?(msg=true) prg =
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 (Global.env ()) Evd.empty x.obl_type ++
+ hov 1 (Printer.pr_constr_env env sigma x.obl_type ++
str "." ++ fnl ())))
| Some _ -> ())
obls
@@ -1086,11 +1092,13 @@ let show_obligations ?(msg=true) n =
let show_term n =
let prg = get_prog_err n in
let n = prg.prg_name in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
(Id.print n ++ spc () ++ str":" ++ spc () ++
- Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
- ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
+ Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+ ++ Printer.pr_constr_env env sigma prg.prg_body)
-let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
+let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
let sign = Decls.initialize_named_context_for_proof () in
@@ -1110,7 +1118,7 @@ let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic
+let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
?(kind=Global,false,Definition) ?(reduce=reduce)
?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
let sign = Decls.initialize_named_context_for_proof () in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 04:18:16 +0000