aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/constr.ml2
-rw-r--r--kernel/term_typing.ml6
-rw-r--r--pretyping/evd.ml6
-rw-r--r--pretyping/evd.mli1
-rw-r--r--pretyping/unification.ml1
-rw-r--r--proofs/pfedit.ml9
-rw-r--r--proofs/pfedit.mli4
-rw-r--r--proofs/proof_global.ml34
-rw-r--r--proofs/proofview.ml2
-rw-r--r--tactics/tacinterp.ml6
-rw-r--r--tactics/tactics.ml25
-rw-r--r--toplevel/obligations.ml4
12 files changed, 63 insertions, 37 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 4f2935be5..13e1abacc 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -471,7 +471,7 @@ let compare_head_gen eq_universes eq_sorts f t1 t2 =
| Rel n1, Rel n2 -> Int.equal n1 n2
| Meta m1, Meta m2 -> Int.equal m1 m2
| Var id1, Var id2 -> Id.equal id1 id2
- | Sort s1, Sort s2 -> Sorts.equal s1 s2
+ | Sort s1, Sort s2 -> eq_sorts s1 s2
| Cast (c1,_,_), _ -> f c1 t2
| _, Cast (c2,_,_) -> f t1 c2
| Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0959fa703..8c4ec8cbf 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -146,7 +146,7 @@ let infer_declaration env kn dcl =
let { const_entry_type = typ; const_entry_opaque = opaque } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let (body, ctx), side_eff = Future.join body in
- let env = push_context_set ctx env in
+ assert(Univ.ContextSet.is_empty ctx);
let body = handle_side_effects env body side_eff in
let def, typ, proj =
match c.const_entry_proj with
@@ -172,9 +172,7 @@ let infer_declaration env kn dcl =
let def = Def (Mod_subst.from_val j.uj_val) in
def, typ, None
in
- let univs = Univ.UContext.union c.const_entry_universes
- (Univ.ContextSet.to_context ctx)
- in
+ let univs = c.const_entry_universes in
feedback_completion_typecheck feedback_id;
def, typ, proj, c.const_entry_polymorphic,
univs, c.const_entry_inline_code, c.const_entry_secctx
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index eda5f66c1..d18568500 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -932,6 +932,12 @@ let merge_uctx rigid uctx ctx' =
let merge_context_set rigid evd ctx' =
{evd with universes = merge_uctx rigid evd.universes ctx'}
+let merge_uctx_subst uctx s =
+ { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
+
+let merge_universe_subst evd subst =
+ {evd with universes = merge_uctx_subst evd.universes subst }
+
let with_context_set rigid d (a, ctx) =
(merge_context_set rigid d ctx, a)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 9be18bc8a..5cc554c26 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -469,6 +469,7 @@ val universes : evar_map -> Univ.universes
val merge_universe_context : evar_map -> evar_universe_context -> evar_map
val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
+val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9e662150e..0ab886ca3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -384,6 +384,7 @@ let is_rigid_head flags t =
match kind_of_term t with
| Const (cst,u) -> not (Cpred.mem cst (snd flags.modulo_delta))
| Ind (i,u) -> true
+ | Fix _ | CoFix _ -> true
| _ -> false
let force_eqs c =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index eeb577025..077057f3c 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -119,13 +119,12 @@ open Decl_kinds
let next = let n = ref 0 in fun () -> incr n; !n
let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
- let substref = ref Univ.LMap.empty in (** FIXME: Something wrong here with subst *)
start_proof id goal_kind sign typ (fun _ -> ());
try
let status = by tac in
- let _,(const,_,_) = cook_proof () in
+ let _,(const,univs,_) = cook_proof () in
delete_current_proof ();
- const, status, !substref
+ const, status, univs
with reraise ->
let reraise = Errors.push reraise in
delete_current_proof ();
@@ -135,11 +134,11 @@ let build_by_tactic env ?(poly=false) typ tac =
let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = val_of_named_context (named_context env) in
let gk = Global, poly, Proof Theorem in
- let ce, status, subst = build_constant_by_tactic id sign ~goal_kind:gk typ tac in
+ let ce, status, univs = build_constant_by_tactic id sign ~goal_kind:gk typ tac in
let ce = Term_typing.handle_side_effects env ce in
let cb, se = Future.force ce.const_entry_body in
assert(Declareops.side_effects_is_empty se);
- cb, status, subst
+ cb, status, fst univs
(**********************************************************************)
(* Support for resolution of evars in tactic interpretation, including
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index e3df619f8..615866c6a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -149,7 +149,9 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
val build_constant_by_tactic :
Id.t -> named_context_val -> ?goal_kind:goal_kind ->
- types Univ.in_universe_context_set -> unit Proofview.tactic -> Entries.definition_entry * bool * Universes.universe_opt_subst
+ types Univ.in_universe_context_set -> unit Proofview.tactic ->
+ Entries.definition_entry * bool * Universes.universe_opt_subst Univ.in_universe_context
+
val build_by_tactic : env -> ?poly:polymorphic ->
types Univ.in_universe_context_set -> unit Proofview.tactic ->
constr Univ.in_universe_context_set * bool * Universes.universe_opt_subst
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 12700851a..e49a57af3 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -264,16 +264,12 @@ let get_open_goals () =
(List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
List.length shelf
-let nf_body nf b =
- let aux ((c, ctx), t) = ((nf c, ctx), t) in
- Future.chain ~pure:true b aux
-
let close_proof ?feedback_id ~now fpl =
let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
let poly = pi2 strength (* Polymorphic *) in
let initial_goals = Proof.initial_goals proof in
let fpl, univs = Future.split2 fpl in
- let (subst, univs as univsubst), nf =
+ let univsubst, make_body =
if poly || now then
let usubst, uctx = Future.force univs in
let ctx, subst =
@@ -286,29 +282,43 @@ let close_proof ?feedback_id ~now fpl =
let subst =
Univ.LMap.union usubst (Univ.LMap.map (fun v -> Some (Univ.Universe.make v)) subst)
in
- (subst, Univ.ContextSet.to_context ctx), nf
+ let univsubst = (subst, Univ.ContextSet.to_context ctx) in
+ let make_body p _c t _octx =
+ let (c, ctx), eff = Future.force p in
+ let body = nf c and typ = nf t in
+ let used_univs =
+ Univ.LSet.union (Universes.universes_of_constr body)
+ (Universes.universes_of_constr typ)
+ in
+ let ctx = Universes.restrict_universe_context ctx used_univs in
+ let p = Future.from_val ((body, Univ.ContextSet.empty),eff) in
+ let univs = Univ.ContextSet.to_context ctx in
+ univs, p, typ
+ in univsubst, make_body
else
let ctx =
List.fold_left (fun acc (c, (t, octx)) ->
Univ.ContextSet.union octx acc)
Univ.ContextSet.empty initial_goals
in
- (Univ.LMap.empty, Univ.ContextSet.to_context ctx), (fun x -> x)
+ let univs = Univ.ContextSet.to_context ctx in
+ let univsubst = (Univ.LMap.empty, univs) in
+ univsubst, (fun p c t octx -> univs, p, t)
in
let entries =
- Future.map2 (fun p (c, (t, octx)) -> { Entries.
- const_entry_body = nf_body nf p;
+ Future.map2 (fun p (c, (t, octx)) ->
+ let univs, body, typ = make_body p c t octx in
+ { Entries.
+ const_entry_body = body;
const_entry_secctx = section_vars;
const_entry_feedback = feedback_id;
- const_entry_type = Some (nf t);
+ const_entry_type = Some typ;
const_entry_inline_code = false;
const_entry_opaque = true;
const_entry_universes = univs;
const_entry_polymorphic = poly;
const_entry_proj = None})
fpl initial_goals in
- if now then
- List.iter (fun x ->ignore(Future.force x.Entries.const_entry_body)) entries;
{ id = pid; entries = entries; persistence = strength; universes = univsubst },
Ephemeron.get terminator
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 291da4a98..83a703a3a 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -838,6 +838,8 @@ struct
let new_evar (evd, evs) env typ =
let src = (Loc.ghost, Evar_kinds.GoalEvar) in
let (evd, ev) = Evarutil.new_evar evd env ~src typ in
+ let evd = Typeclasses.mark_unresolvables
+ ~filter:(fun ev' _ -> Evar.equal (fst (Term.destEvar ev)) ev') evd in
let (evk, _) = Term.destEvar ev in
let h = (evd, build_goal evk :: evs) in
(h, ev)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f32c06ba4..a4d840cf0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1807,14 +1807,16 @@ and interp_atomic ist tac =
extend_gl_hyps) is incorrect. This means that evar
instantiated by pf_interp_constr may be lost, there. *)
let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
- let (_,c_interp) =
+ let (sigma',c_interp) =
try pf_interp_constr ist (extend_gl_hyps gl sign) c
with e when to_catch e (* Hack *) ->
errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
in
tclTHEN
(tclEVARS sigma)
- (Tactics.change (Some op) c_interp (interp_clause ist env cl))
+ (tclTHEN (* At least recover the declared universes *)
+ (tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context sigma'))
+ (Tactics.change (Some op) c_interp (interp_clause ist env cl)))
gl
end
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 024165fd0..0fbb511a7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3720,7 +3720,7 @@ let interpretable_as_section_decl d1 d2 = match d2,d1 with
| (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 && eq_constr t1 t2
| (_,None,t1), (_,_,t2) -> eq_constr t1 t2
-let abstract_subproof id tac =
+let abstract_subproof id gk tac =
let open Tacticals.New in
let open Tacmach.New in
let open Proofview.Notations in
@@ -3749,8 +3749,8 @@ let abstract_subproof id tac =
evd, ctx, nf concl
in
let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
- let (const, safe, subst) =
- try Pfedit.build_constant_by_tactic id secsign (concl, ctx) solve_tac
+ let (const, safe, (subst, ctx)) =
+ try Pfedit.build_constant_by_tactic ~goal_kind:gk id secsign (concl, ctx) solve_tac
with Proof_errors.TacticFailure e as src ->
(* if the tactic [tac] fails, it reports a [TacticFailure e],
which is an error irrelevant to the proof system (in fact it
@@ -3766,7 +3766,8 @@ let abstract_subproof id tac =
let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
(* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
- let evd = Evd.merge_context_set Evd.univ_flexible evd (Univ.ContextSet.of_context ctx) in
+ let evd = Evd.merge_context_set Evd.univ_rigid evd (Univ.ContextSet.of_context ctx) in
+ let evd = Evd.merge_universe_subst evd subst in
let open Declareops in
let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
let effs = cons_side_effects eff no_seff in
@@ -3780,14 +3781,18 @@ let anon_id = Id.of_string "anonymous"
let tclABSTRACT name_op tac =
let open Proof_global in
- let s = match name_op with
- | Some s -> s
+ let default_gk = (Global, false, Proof Theorem) in
+ let s, gk = match name_op with
+ | Some s ->
+ (try let _, gk, _ = current_proof_statement () in s, gk
+ with NoCurrentProof -> s, default_gk)
| None ->
- let name = try get_current_proof_name () with NoCurrentProof -> anon_id in
- add_suffix name "_subproof"
+ let name, gk =
+ try let name, gk, _ = current_proof_statement () in name, gk
+ with NoCurrentProof -> anon_id, default_gk in
+ add_suffix name "_subproof", gk
in
- abstract_subproof s tac
-
+ abstract_subproof s gk tac
let admit_as_an_axiom =
Proofview.tclUNIT () >>= fun () -> (* delay for Coqlib.build_coq_proof_admitted *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index d45c2af3e..cce5242ec 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -791,8 +791,8 @@ let rec string_of_list sep f = function
let solve_by_tac name evi t poly subst ctx =
let id = name in
let concl = Universes.subst_opt_univs_constr subst evi.evar_concl in
- (* spiwack: the status is dropped *)
- let (entry,_,subst) = Pfedit.build_constant_by_tactic
+ (* spiwack: the status is dropped. MS: the ctx is dropped too *)
+ let (entry,_,(subst,ctx)) = Pfedit.build_constant_by_tactic
id ~goal_kind:(goal_kind poly) evi.evar_hyps (concl, ctx) (Tacticals.New.tclCOMPLETE t) in
let env = Global.env () in
let entry = Term_typing.handle_side_effects env entry in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 18:01:13 +0000