summaryrefslogtreecommitdiff
path: root/toplevel/obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/obligations.ml')
-rw-r--r--toplevel/obligations.ml43
1 files changed, 27 insertions, 16 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 9019f486..314789ce 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -318,8 +318,9 @@ type program_info_aux = {
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
- prg_hook : unit Lemmas.declaration_hook;
+ prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook;
prg_opaque : bool;
+ prg_sign: named_context_val;
}
type program_info = program_info_aux Ephemeron.key
@@ -517,7 +518,7 @@ let declare_definition prg =
progmap_remove prg;
!declare_definition_ref prg.prg_name
prg.prg_kind ce prg.prg_implicits
- (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r))
+ (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
open Pp
@@ -582,6 +583,7 @@ let declare_mutual_definition l =
in
(* Declare the recursive definitions *)
let ctx = Evd.evar_context_universe_context first.prg_ctx in
+ let fix_exn = Stm.get_fix_exn () in
let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
@@ -589,8 +591,8 @@ let declare_mutual_definition l =
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 (fun exn -> exn) first.prg_hook local gr;
- List.iter progmap_remove l; kn
+ Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
+ List.iter progmap_remove l; kn
let shrink_body c =
let ctx, b = decompose_lam c in
@@ -642,7 +644,7 @@ let declare_obligation prg obl body ty uctx =
else
Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
-let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls kind reduce hook =
+let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls impls kind reduce hook =
let obls', b =
match b with
| None ->
@@ -666,8 +668,8 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls
prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
prg_implicits = impls; prg_kind = kind; prg_reduce = reduce;
- prg_hook = hook;
- prg_opaque = opaque; }
+ prg_hook = hook; prg_opaque = opaque;
+ prg_sign = sign }
let map_cardinal m =
let i = ref 0 in
@@ -822,7 +824,9 @@ let obligation_hook prg obl num auto ctx' _ gr =
if not (pi2 prg.prg_kind) (* Not polymorphic *) then
(* The universe context was declared globally, we continue
from the new global environment. *)
- Evd.evar_universe_context (Evd.from_env (Global.env ()))
+ let evd = Evd.from_env (Global.env ()) in
+ let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
+ Evd.evar_universe_context ctx'
else ctx'
in
let prg = { prg with prg_ctx = ctx' } in
@@ -853,9 +857,10 @@ let rec solve_obligation prg num tac =
let obl = subst_deps_obl obls obl in
let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
let evd = Evd.from_ctx prg.prg_ctx in
+ let evd = Evd.update_sigma_env evd (Global.env ()) in
let auto n tac oblset = auto_solve_obligations n ~oblset tac in
let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
- let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type hook in
+ let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type hook in
let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in
let _ = Pfedit.by (snd (get_default_tactic ())) in
@@ -889,17 +894,21 @@ and solve_obligation_by_tac prg obls i tac =
| Some t -> t
| None -> snd (get_default_tactic ())
in
+ let evd = Evd.from_ctx !prg.prg_ctx in
+ let evd = Evd.update_sigma_env evd (Global.env ()) in
let t, ty, ctx =
solve_by_tac obl.obl_name (evar_of_obligation obl) tac
- (pi2 !prg.prg_kind) !prg.prg_ctx
+ (pi2 !prg.prg_kind) (Evd.evar_universe_context evd)
in
let uctx = Evd.evar_context_universe_context 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 (pi2 !prg.prg_kind) then (
- (* Declare the term constraints with the first obligation only *)
- let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in
+ (* Declare the term constraints with the first obligation only *)
+ 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
prg := {!prg with prg_ctx = ctx'});
true
else false
@@ -987,9 +996,10 @@ let show_term n =
++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls =
+ ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
+ let sign = Decls.initialize_named_context_for_proof () in
let info = str (Id.to_string n) ++ str " has type-checked" in
- let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
+ let prg = init_prog_info sign ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose msg_info (info ++ str ".");
@@ -1005,11 +1015,12 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
| _ -> res)
let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
- ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind =
+ ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
+ let sign = Decls.initialize_named_context_for_proof () in
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 (Some b) t ctx deps (Some fixkind)
+ let prg = init_prog_info sign ~opaque n (Some b) t ctx deps (Some fixkind)
notations obls imps kind reduce hook
in progmap_add n (Ephemeron.create prg)) l;
let _defined =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 15:18:03 +0000