diff options
25 files changed, 111 insertions, 141 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 77e34d4e00..f434b63d74 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -596,7 +596,7 @@ plugin:ci-elpi: plugin:ci-equations: <<: *ci-template -plugin:ci-fiat-parsers: +plugin:ci-fiat_parsers: <<: *ci-template plugin:ci-ltac2: diff --git a/Makefile.ci b/Makefile.ci index b8bff98f5f..0307d39d54 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -25,7 +25,7 @@ CI_TARGETS= \ ci-fcsl-pcm \ ci-fiat-crypto \ ci-fiat-crypto-legacy \ - ci-fiat-parsers \ + ci-fiat_parsers \ ci-flocq \ ci-geocoq \ ci-coqhammer \ diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat_parsers.sh index ac74ebf667..ac74ebf667 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat_parsers.sh diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh deleted file mode 100644 index 6e89741e29..0000000000 --- a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then - - bignums_CI_REF=primitive-integers - bignums_CI_GITURL=https://github.com/vbgl/bignums - - mtac2_CI_REF=primitive-integers - mtac2_CI_GITURL=https://github.com/vbgl/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh deleted file mode 100644 index 2df8affd14..0000000000 --- a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then - - elpi_CI_REF=ltac+remove_aliases - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh deleted file mode 100644 index f2a113b118..0000000000 --- a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then - - mtac2_CI_REF=build+warn_50 - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh deleted file mode 100644 index f532fdfc52..0000000000 --- a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then - - ltac2_CI_REF=proof_rework - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - mtac2_CI_REF=proof_rework - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh new file mode 100644 index 0000000000..23eb24c304 --- /dev/null +++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then + + ltac2_CI_REF=proofview+proof_info + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + fiat_parsers_CI_REF=proofview+proof_info + fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat + +fi diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh deleted file mode 100644 index efcdd2e97f..0000000000 --- a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then - - paramcoq_CI_REF=stm-shallow-logic - paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq - -fi diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh deleted file mode 100644 index ebd1b524da..0000000000 --- a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then - - mtac2_CI_REF=proof-mode - mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 - - ltac2_CI_REF=proof-mode - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - equations_CI_REF=proof-mode - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh b/dev/ci/user-overlays/09410-maximedenes-thread-program.sh deleted file mode 100644 index 985c2db74e..0000000000 --- a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh +++ /dev/null @@ -1,13 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9410" ] || [ "$CI_BRANCH" = "thread-program" ]; then - - math_classes_CI_REF=program-mode-flag - math_classes_CI_GITURL=https://github.com/maximedenes/math-classes - - ltac2_CI_REF=program-mode-flag - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - - equations_CI_REF=thread-program - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/engine/proofview.ml b/engine/proofview.ml index d4ad53ff5f..a725444e81 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -223,9 +223,9 @@ module Proof = Logical type +'a tactic = 'a Proof.t (** Applies a tactic to the current proofview. *) -let apply env t sp = +let apply ~name ~poly env t sp = let open Logic_monad in - let ans = Proof.repr (Proof.run t false (sp,env)) in + let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in let ans = Logic_monad.NonLogical.run ans in match ans with | Nil (e, info) -> iraise (TacticFailure e, info) @@ -993,7 +993,10 @@ let tclTIME s t = tclOR (tclUNIT x) (fun e -> aux (n+1) (k e)) in aux 0 t - +let tclProofInfo = + let open Proof in + Logical.current >>= fun P.{name; poly} -> + tclUNIT (name, poly) (** {7 Unsafe primitives} *) @@ -1275,7 +1278,8 @@ module V82 = struct let of_tactic t gls = try let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in - let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in + let name, poly = Names.Id.of_string "legacy_pe", false in + let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> let (_, info) = CErrors.push src in diff --git a/engine/proofview.mli b/engine/proofview.mli index 286703c0dc..680a93f0cc 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -156,10 +156,15 @@ type +'a tactic tactic has given up. In case of multiple success the first one is selected. If there is no success, fails with {!Logic_monad.TacticFailure}*) -val apply : Environ.env -> 'a tactic -> proofview -> 'a - * proofview - * (bool*Evar.t list*Evar.t list) - * Proofview_monad.Info.tree +val apply + : name:Names.Id.t + -> poly:bool + -> Environ.env + -> 'a tactic + -> proofview + -> 'a * proofview + * (bool*Evar.t list*Evar.t list) + * Proofview_monad.Info.tree (** {7 Monadic primitives} *) @@ -407,6 +412,10 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic identifying annotation if present *) val tclTIME : string option -> 'a tactic -> 'a tactic +(** Internal, don't use. *) +val tclProofInfo : (Names.Id.t * bool) tactic +[@@ocaml.deprecated "internal, don't use"] + (** {7 Unsafe primitives} *) (** The primitives in the [Unsafe] module should be avoided as much as diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 69341d97df..80eb9d0124 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -177,7 +177,7 @@ module P = struct type s = proofview * Environ.env (** Recording info trace (true) or not. *) - type e = bool + type e = { trace: bool; name : Names.Id.t; poly : bool } (** Status (safe/unsafe) * shelved goals * given up *) type w = bool * goal list @@ -254,13 +254,16 @@ end (** Lens and utilies pertaining to the info trace *) module InfoL = struct - let recording = Logical.current + let recording = Logical.(map (fun {P.trace} -> trace) current) let if_recording t = let open Logical in recording >>= fun r -> if r then t else return () - let record_trace t = Logical.local true t + let record_trace t = + Logical.( + current >>= fun s -> + local {s with P.trace = true} t) let raw_update = Logical.update let update f = if_recording (raw_update f) diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index a08cab3bf6..3437b6ce77 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -98,7 +98,7 @@ module P : sig val wprod : w -> w -> w (** Recording info trace (true) or not. *) - type e = bool + type e = { trace: bool; name : Names.Id.t; poly : bool } type u = Info.state diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 525ff7fd0f..62906303a4 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -530,7 +530,15 @@ let interp_gen kind ist pattern_mode flags env sigma c = invariant that running the tactic returned by push_trace does not modify sigma. *) let (_, dummy_proofview) = Proofview.init sigma [] in - let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in + + (* Again this is called at times with no open proof! *) + let name, poly = + try + let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in + name, poly + with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false + in + let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) term in @@ -2041,7 +2049,16 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in - let name, poly = Id.of_string "ltac_sub", false in + (* XXX: This depends on the global state which is bad; the hooking + mechanism should be modified. *) + let name, poly = + try + let (_, poly, _) = Proof_global.get_current_persistence () in + let name = Proof_global.get_current_proof_name () in + name, poly + with | Proof_global.NoCurrentProof -> + Id.of_string "ltac_gen", false + in let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7f1ae6d12b..9509c36ec0 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -70,11 +70,6 @@ let get_current_context ?p () = let evd = Proof.in_proof p (fun x -> x) in (evd, Global.env ()) -let current_proof_statement () = - match Proof_global.V82.get_current_initial_conclusions () with - | (id,([concl],strength)) -> id,strength,concl - | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.") - let solve ?with_end_tac gi info_lvl tac pr = try let tac = match with_end_tac with diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 5699320af5..29ab00876a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -34,11 +34,6 @@ val get_current_goal_context : unit -> Evd.evar_map * env val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env -(** [current_proof_statement] *) - -val current_proof_statement : - unit -> Id.t * goal_kind * EConstr.types - (** {6 ... } *) (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th diff --git a/proofs/proof.ml b/proofs/proof.ml index 4ce932b93d..e40940f652 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -415,8 +415,9 @@ let run_tactic env tac pr = Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved in + let { name; poly } = pr in let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = - Proofview.apply env tac sp + Proofview.apply ~name ~poly env tac sp in let sigma = Proofview.return proofview in let to_shelve = undef sigma to_shelve in @@ -498,7 +499,8 @@ module V82 = struct let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in Proofview.Unsafe.tclEVARS sigma end in - let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in + let { name; poly } = pr in + let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in let shelf = List.filter begin fun g -> Evd.is_undefined (Proofview.return proofview) g diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9ee9e7ae2c..0cfc010c1a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -66,12 +66,6 @@ let pstates = ref ([] : pstate list) (* combinators for the current_proof lists *) let push a l = l := a::!l -exception NoSuchProof -let () = CErrors.register_handler begin function - | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") - | _ -> raise CErrors.Unhandled -end - exception NoCurrentProof let () = CErrors.register_handler begin function | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") @@ -91,6 +85,7 @@ let cur_pstate () = let give_me_the_proof () = (cur_pstate ()).proof let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name +let get_current_persistence () = (cur_pstate ()).strength let with_current_proof f = match !pstates with @@ -386,15 +381,6 @@ let set_terminator hook = | [] -> raise NoCurrentProof | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps -module V82 = struct - let get_current_initial_conclusions () = - let { proof; strength } = cur_pstate () in - let Proof.{ name; entry } = Proof.data proof in - let initial = Proofview.initial_goals entry in - let goals = List.map (fun (o, c) -> c) initial in - name, (goals, strength) -end - let freeze ~marshallable = if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") else !pstates diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 40920f51a3..38e234eaee 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -17,6 +17,7 @@ val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.Id.t +val get_current_persistence : unit -> Decl_kinds.goal_kind val get_all_proof_names : unit -> Names.Id.t list val discard : Names.lident -> unit @@ -104,8 +105,6 @@ val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> val get_terminator : unit -> proof_terminator val set_terminator : proof_terminator -> unit -exception NoSuchProof - val get_open_goals : unit -> int (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is @@ -129,11 +128,6 @@ val get_used_variables : unit -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : unit -> UState.universe_decl -module V82 : sig - val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * - Decl_kinds.goal_kind) -end - val freeze : marshallable:bool -> t val unfreeze : t -> unit val proof_of_state : t -> Proof.t diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 3a687a6b41..c3e3a62e26 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -11,7 +11,6 @@ module CVars = Vars open Util -open Names open Termops open EConstr open Decl_kinds @@ -87,10 +86,26 @@ let shrink_entry sign const = } in (const, args) -let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = +let name_op_to_name ~name_op ~name ~goal_kind suffix = + match name_op with + | Some s -> s, goal_kind + | None -> Nameops.add_suffix name suffix, goal_kind + +let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (name, poly) -> + (* This is important: The [Global] and [Proof Theorem] parts of the + goal_kind are not relevant here as build_constant_by_tactic does + use the noop terminator; but beware if some day we remove the + redundancy on constrant declaration. This opens up an interesting + question, how does abstract behave when discharge is local for example? + *) + let goal_kind, suffix = if opaque + then (Global,poly,Proof Theorem), "_subproof" + else (Global,poly,DefinitionBody Definition), "_subterm" in + let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -126,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in let ectx = Evd.evar_universe_context evd in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~goal_kind id ectx secsign concl solve_tac with Logic_monad.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 @@ -170,26 +185,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac end -let abstract_subproof ~opaque id gk tac = - cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> Tactics.exact_no_check (applist (lem, args))) - -let anon_id = Id.of_string "anonymous" - -let name_op_to_name name_op object_kind suffix = - let open Proof_global in - let default_gk = (Global, false, object_kind) in - let name, gk = match Proof_global.V82.get_current_initial_conclusions () with - | (id, (_, gk)) -> Some id, gk - | exception NoCurrentProof -> None, default_gk - in - match name_op with - | Some s -> s, gk - | None -> - let name = Option.default anon_id name in - Nameops.add_suffix name suffix, gk +let abstract_subproof ~opaque tac = + cache_term_by_tactic_then ~opaque tac (fun lem args -> Tactics.exact_no_check (applist (lem, args))) let tclABSTRACT ?(opaque=true) name_op tac = - let s, gk = if opaque - then name_op_to_name name_op (Proof Theorem) "_subproof" - else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in - abstract_subproof ~opaque s gk tac + abstract_subproof ~opaque ~name_op tac diff --git a/tactics/abstract.mli b/tactics/abstract.mli index 7fb671fbf8..9d4f3cfb27 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -11,6 +11,12 @@ open Names open EConstr -val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic +val cache_term_by_tactic_then + : opaque:bool + -> name_op:Id.t option + -> ?goal_type:(constr option) + -> unit Proofview.tactic + -> (constr -> constr list -> unit Proofview.tactic) + -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ba7645446d..e505bb3a42 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -930,8 +930,16 @@ module Search = struct let _, pv = Proofview.init evm [] in let pv = Proofview.unshelve goals pv in try + (* Instance may try to call this before a proof is set up! + Thus, give_me_the_proof will fail. Beware! *) + let name, poly = try + let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in + name, poly + with | Proof_global.NoCurrentProof -> + Id.of_string "instance", false + in let (), pv', (unsafe, shelved, gaveup), _ = - Proofview.apply env tac pv + Proofview.apply ~name ~poly env tac pv in if not (List.is_empty gaveup) then CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 4635883dc2..79182a3f9d 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -481,7 +481,14 @@ let save_proof ?proof = function Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> let pftree = Proof_global.give_me_the_proof () in - let id, k, typ = Pfedit.current_proof_statement () in + let gk = Proof_global.get_current_persistence () in + let Proof.{ name; poly; entry } = Proof.data pftree in + let typ = match Proofview.initial_goals entry with + | [typ] -> snd typ + | _ -> + CErrors.anomaly + ~label:"Lemmas.save_proof" (Pp.str "more than one statement.") + in let typ = EConstr.Unsafe.to_constr typ in let universes = Proof.((data pftree).initial_euctx) in (* This will warn if the proof is complete *) @@ -491,16 +498,15 @@ let save_proof ?proof = function if not !keep_admitted_vars then None else match Proof_global.get_used_variables(), pproofs with | Some _ as x, _ -> x - | None, (pproof, _) :: _ -> + | None, (pproof, _) :: _ -> let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in let ids_def = Environ.global_vars_set env pproof in Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in let decl = Proof_global.get_universe_decl () in - let poly = pi2 k in let ctx = UState.check_univ_decl ~poly universes decl in - Admitted(id,k,(sec_vars, (typ, ctx), None), universes) + Admitted(name,gk,(sec_vars, (typ, ctx), None), universes) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (opaque,idopt) -> |