diff options
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 68 |
1 files changed, 37 insertions, 31 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 765d6851..2f7dee9a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -40,7 +40,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: Context.Named.t; + ev_hyps: Constr.named_context; ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; @@ -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 @@ -218,7 +220,7 @@ let eterm_obligations env name evm fs ?status t ty = in let loc, k = evar_source id evm in let status = match k with - | Evar_kinds.QuestionMark (o,_) -> o + | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o | _ -> match status with | Some o -> o | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ())) @@ -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 ; @@ -338,7 +342,7 @@ open Goptions let _ = declare_bool_option { optdepr = false; - optname = "Hidding of Program obligations"; + optname = "Hiding of Program obligations"; optkey = ["Hide";"Obligations"]; optread = get_hide_obligations; optwrite = set_hide_obligations; } @@ -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,16 +474,15 @@ 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 let typ = nf typ in let body = nf body in - let env = Global.env () in let uvars = Univ.LSet.union - (Univops.universes_of_constr env typ) - (Univops.universes_of_constr env body) in + (Univops.universes_of_constr typ) + (Univops.universes_of_constr body) in let uctx = UState.restrict prg.prg_ctx uvars in let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in @@ -555,7 +558,7 @@ 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; @@ -611,7 +614,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 @@ -743,7 +746,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 @@ -814,10 +817,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 @@ -849,12 +851,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 = @@ -893,7 +895,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) @@ -1071,9 +1073,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 @@ -1089,11 +1093,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 @@ -1113,7 +1119,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 |