aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/lemmas.ml')
-rw-r--r--vernac/lemmas.ml80
1 files changed, 37 insertions, 43 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 645320c60..192dd027c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -11,7 +11,6 @@
open CErrors
open Util
-open Flags
open Pp
open Names
open Term
@@ -49,7 +48,7 @@ let retrieve_first_recthm uctx = function
(NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
| ConstRef cst ->
let cb = Global.lookup_constant cst in
- let (_, uctx) = UState.universe_context uctx in
+ let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in
let inst = Univ.UContext.instance uctx in
let map (c, ctx) = Vars.subst_instance_constr inst c in
(Option.map map (Global.body_of_constant_body cb), is_opaque cb)
@@ -137,7 +136,7 @@ let find_mutually_recursive_statements thms =
assert (List.is_empty rest);
(* One occ. of common coind ccls and no common inductive hyps *)
if not (List.is_empty common_same_indhyp) then
- if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
+ Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
flush_all ();
indccl, true, []
| [], _::_ ->
@@ -145,7 +144,7 @@ let find_mutually_recursive_statements thms =
| ind :: _ ->
if List.distinct_f ind_ord (List.map pi1 ind)
then
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(strbrk
("Coinductive statements do not follow the order of "^
"definition, assuming the proof to be by induction."));
@@ -210,11 +209,11 @@ let compute_proof_name locality = function
locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
then
user_err ?loc (pr_id id ++ str " already exists.");
- id, pl
+ id
| None ->
- next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None
+ next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ())
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
match body with
| None ->
@@ -222,7 +221,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
| Discharge ->
let impl = false in (* copy values from Vernacentries *)
let k = IsAssumption Conjectural in
- let c = SectionLocalAssum ((t_i,ctx),p,impl) in
+ let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in
let _ = declare_variable id (Lib.cwd(),c,k) in
(Discharge, VarRef id,imps)
| Local | Global ->
@@ -232,7 +231,6 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
| Global -> false
| Discharge -> assert false
in
- let ctx = Univ.ContextSet.to_context ctx in
let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
let kn = declare_constant id ~local decl in
(locality,ConstRef kn,imps))
@@ -250,12 +248,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
match locality with
| Discharge ->
let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p
- ~univs:(Univ.ContextSet.to_context ctx) body_i in
+ ~univs:ctx body_i in
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
(Discharge,VarRef id,imps)
| Local | Global ->
- let ctx = Univ.ContextSet.to_context ctx in
let local = match locality with
| Local -> true
| Global -> false
@@ -312,12 +309,6 @@ let get_proof proof do_guard hook opacity =
in
id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-let check_exist =
- List.iter (fun (loc,id) ->
- if not (Nametab.exists_cci (Lib.make_path id)) then
- user_err ?loc (pr_id id ++ str " does not exist.")
- )
-
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
@@ -325,17 +316,16 @@ let universe_proof_terminator compute_guard hook =
admit (id,k,pe) pl (hook (Some ctx)) ();
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
- let is_opaque, export_seff, exports = match opaque with
- | Vernacexpr.Transparent -> false, true, []
- | Vernacexpr.Opaque None -> true, false, []
- | Vernacexpr.Opaque (Some l) -> true, true, l in
+ let is_opaque, export_seff = match opaque with
+ | Vernacexpr.Transparent -> false, true
+ | Vernacexpr.Opaque -> true, false
+ in
let proof = get_proof proof compute_guard
(hook (Some (fst proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
| Some (_,id) -> save_anonymous ~export_seff proof id
- end;
- check_exist exports
+ end
end
let standard_proof_terminator compute_guard hook =
@@ -369,7 +359,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
let rec_tac_initializer finite guard thms snl =
if finite then
- match List.map (fun ((id,_),(t,_)) -> (id,EConstr.of_constr t)) thms with
+ match List.map (fun (id,(t,_)) -> (id,EConstr.of_constr t)) thms with
| (id,_)::l -> Tactics.mutual_cofix id l 0
| _ -> assert false
else
@@ -377,11 +367,11 @@ let rec_tac_initializer finite guard thms snl =
let nl = match snl with
| None -> List.map succ (List.map List.last guard)
| Some nl -> nl
- in match List.map2 (fun ((id,_),(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
+ in match List.map2 (fun (id,(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
-let start_proof_with_initialization kind ctx recguard thms snl hook =
+let start_proof_with_initialization kind ctx decl recguard thms snl hook =
let intro_tac (_, (_, (ids, _))) =
Tacticals.New.tclMAP (function
| Name id -> Tactics.intro_mustbe_force id
@@ -406,7 +396,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
(if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
match thms with
| [] -> anomaly (Pp.str "No proof to start.")
- | ((id,pl),(t,(_,imps)))::other_thms ->
+ | (id,(t,(_,imps)))::other_thms ->
let hook ctx strength ref =
let ctx = match ctx with
| None -> Evd.empty_evar_universe_context
@@ -418,22 +408,24 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let body,opaq = retrieve_first_recthm ctx ref in
let subst = Evd.evar_universe_context_subst ctx in
let norm c = Universes.subst_opt_univs_constr subst c in
- let ctx = UState.context_set (*FIXME*) ctx in
+ let binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
let body = Option.map norm body in
- List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
+ List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
call_hook (fun exn -> exn) hook strength ref) thms_data in
- start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+ start_proof_univs id ~pl:decl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
let start_proof_com ?inference_hook kind thms hook =
let env0 = Global.env () in
- let levels = Option.map snd (fst (List.hd thms)) in
- let evdref = ref (match levels with
- | None -> Evd.from_env env0
- | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
- in
+ let decl = fst (List.hd thms) in
+ let evd, decl =
+ match decl with
+ | None -> Evd.from_env env0, Univdecls.default_univ_decl
+ | Some decl ->
+ Univdecls.interp_univ_decl_opt env0 (snd decl) in
+ let evdref = ref evd in
let thms = List.map (fun (sopt,(bl,t)) ->
let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
let t', imps' = interp_type_evars_impls ~impls env evdref t in
@@ -449,16 +441,16 @@ let start_proof_com ?inference_hook kind thms hook =
let evd, nf = Evarutil.nf_evars_and_universes !evdref in
let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
let () =
- match levels with
- | None -> ()
- | Some l -> ignore (Evd.universe_context evd ?names:l)
+ if not decl.Misctypes.univdecl_extensible_instance then
+ ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false)
+ else ()
in
let evd =
if pi2 kind then evd
else (* We fix the variables to ensure they won't be lowered to Set *)
Evd.fix_undefined_variables evd
in
- start_proof_with_initialization kind evd recguard thms snl hook
+ start_proof_with_initialization kind evd decl recguard thms snl hook
(* Saving a proof *)
@@ -507,11 +499,13 @@ let save_proof ?proof = function
let ids_def = Environ.global_vars_set env pproof in
Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
| _ -> None in
- let names = Proof_global.get_universe_binders () in
+ let decl = Proof_global.get_universe_decl () in
let evd = Evd.from_ctx universes in
- let binders, ctx = Evd.universe_context ?names evd in
- Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
- (universes, Some binders))
+ let binders, ctx = Evd.check_univ_decl evd decl in
+ let poly = pi2 k in
+ let binders = if poly then Some binders else None in
+ Admitted(id,k,(sec_vars, poly, (typ, ctx), None),
+ (universes, binders))
in
Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
| Vernacexpr.Proved (is_opaque,idopt) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 18:04:03 +0000