diff options
38 files changed, 442 insertions, 194 deletions
diff --git a/clib/cMap.ml b/clib/cMap.ml index baac892b9e..8d822667c3 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -58,6 +58,7 @@ module MapExt (M : Map.OrderedType) : sig type 'a map = 'a Map.Make(M).t val set : M.t -> 'a -> 'a map -> 'a map + val get : M.t -> 'a map -> 'a val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map val domain : 'a map -> Set.Make(M).t val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map @@ -124,6 +125,14 @@ struct if r == r' then s else map_inj (MNode {l; v=k'; d=v'; r=r'; h}) + let rec get k (s:'a map) : 'a = match map_prj s with + | MEmpty -> assert false + | MNode {l; v=k'; d=v; r; h} -> + let c = M.compare k k' in + if c < 0 then get k l + else if c = 0 then v + else get k r + let rec modify k f (s : 'a map) : 'a map = match map_prj s with | MEmpty -> raise Not_found | MNode {l; v; d; r; h} -> @@ -324,5 +333,4 @@ module Make(M : Map.OrderedType) = struct include Map.Make(M) include MapExt(M) - let get k m = try find k m with Not_found -> assert false end diff --git a/clib/hMap.ml b/clib/hMap.ml index f77068b477..9858477489 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -367,7 +367,10 @@ struct | None -> None | Some m -> Map.find_opt k m - let get k s = try find k s with Not_found -> assert false + let get k s = + let h = M.hash k in + let m = Int.Map.get h s in + Map.get k m let split k s = assert false (** Cannot be implemented efficiently *) diff --git a/clib/int.ml b/clib/int.ml index ee4b3128d5..e0dbfb5274 100644 --- a/clib/int.ml +++ b/clib/int.ml @@ -42,6 +42,13 @@ struct else if i = k then v else find i r + let rec get i s = match map_prj s with + | MEmpty -> assert false + | MNode (l, k, v, r, h) -> + if i < k then get i l + else if i = k then v + else get i r + let rec find_opt i s = match map_prj s with | MEmpty -> None | MNode (l, k, v, r, h) -> diff --git a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh new file mode 100644 index 0000000000..f4840c2a83 --- /dev/null +++ b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10681" ] || [ "$CI_BRANCH" = "proof+private_entry" ]; then + + equations_CI_REF=proof+private_entry + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst new file mode 100644 index 0000000000..09bef82c80 --- /dev/null +++ b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst @@ -0,0 +1,11 @@ +- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + only run their tactic argument once, even if it has multiple + successes. This prevents blow-up and looping from using + multisuccess tactics with :tacn:`assert_succeeds`. (`#10966 + <https://github.com/coq/coq/pull/10966>`_ fixes `#10965 + <https://github.com/coq/coq/issues/10965>`_, by Jason Gross). + +- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + behave correctly when their tactic fully solves the goal. (`#10966 + <https://github.com/coq/coq/pull/10966>`_ fixes `#9114 + <https://github.com/coq/coq/issues/9114>`_, by Jason Gross). diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst new file mode 100644 index 0000000000..c1df728c5c --- /dev/null +++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst @@ -0,0 +1,6 @@ +- Optionally highlight the differences between successive proof steps in the + :cmd:`Show Proof` command. Experimental; only available in coqtop + and Proof General for now, may be supported in other IDEs + in the future. + (`#10494 <https://github.com/coq/coq/pull/10494>`_, + by Jim Fehrle). diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 79eddbd3b5..6efc634087 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -516,7 +516,9 @@ Coq provides a derived tactic to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr :name: assert_fails - This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`. + This behaves like :tacn:`idtac` if :n:`@ltac_expr` fails, and + behaves like :n:`fail 0 @ltac_expr "succeeds"` if :n:`@ltac_expr` + has at least one success. Checking the success ~~~~~~~~~~~~~~~~~~~~ @@ -528,7 +530,7 @@ success: :name: assert_succeeds This behaves like - :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`. + :n:`tryif (assert_fails @ltac_expr) then fail 0 @ltac_expr "fails" else idtac`. Solving ~~~~~~~ diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 57a54bc0ad..00f8269dc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,7 +535,7 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Proof + .. cmdv:: Show Proof {? Diffs {? removed } } :name: Show Proof Displays the proof term generated by the tactics @@ -544,6 +544,12 @@ Requesting information constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier. + Experimental: Specifying “Diffs” highlights the difference between the + current and previous proof step. By default, the command shows the + output once with additions highlighted. Including “removed” shows + the output twice: once showing removals and once showing additions. + It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. + .. cmdv:: Show Conjectures :name: Show Conjectures @@ -624,8 +630,11 @@ Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps and between -values in some error messages. +Coq can automatically highlight the differences between successive proof steps +and between values in some error messages. Also, as an experimental feature, +Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` +command, but only, for now, when using coqtop and Proof General. + For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added diff --git a/kernel/environ.ml b/kernel/environ.ml index 98d66cafa1..2bee2f7a8e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -231,22 +231,26 @@ let fold_inductives f env acc = (* Global constants *) let lookup_constant_key kn env = - Cmap_env.find kn env.env_globals.Globals.constants + Cmap_env.get kn env.env_globals.Globals.constants let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.Globals.constants) + fst (lookup_constant_key kn env) + +let mem_constant kn env = Cmap_env.mem kn env.env_globals.Globals.constants (* Mutual Inductives *) +let lookup_mind_key kn env = + Mindmap_env.get kn env.env_globals.Globals.inductives + let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.Globals.inductives) + fst (lookup_mind_key kn env) + +let mem_mind kn env = Mindmap_env.mem kn env.env_globals.Globals.inductives let mind_context env mind = let mib = lookup_mind mind env in Declareops.inductive_polymorphic_context mib -let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.Globals.inductives - let oracle env = env.env_typing_flags.conv_oracle let set_oracle env o = let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in diff --git a/kernel/environ.mli b/kernel/environ.mli index 5af2a7288b..782ea1c666 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -201,10 +201,12 @@ val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_in val lookup_constant_key : Constant.t -> env -> constant_key (** Looks up in the context of global constant names - raises [Not_found] if the required path is not found *) + raises an anomaly if the required path is not found *) val lookup_constant : Constant.t -> env -> Opaqueproof.opaque constant_body val evaluable_constant : Constant.t -> env -> bool +val mem_constant : Constant.t -> env -> bool + (** New-style polymorphism *) val polymorphic_constant : Constant.t -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool @@ -215,7 +217,7 @@ val type_in_type_constant : Constant.t -> env -> bool [c] is opaque, [NotEvaluableConst NoBody] if it has no body, [NotEvaluableConst IsProj] if [c] is a projection, [NotEvaluableConst (IsPrimitive p)] if [c] is primitive [p] - and [Not_found] if it does not exist in [env] *) + and an anomaly if it does not exist in [env] *) type const_evaluation_result = | NoBody @@ -254,9 +256,11 @@ val add_mind_key : MutInd.t -> mind_key -> env -> env val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names - raises [Not_found] if the required path is not found *) + raises an anomaly if the required path is not found *) val lookup_mind : MutInd.t -> env -> mutual_inductive_body +val mem_mind : MutInd.t -> env -> bool + (** The universe context associated to the inductive, empty if not polymorphic *) val mind_context : env -> MutInd.t -> Univ.AUContext.t diff --git a/kernel/names.ml b/kernel/names.ml index 9802d4f531..b755ff0e08 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -675,6 +675,7 @@ module InductiveOrdered_env = struct end module Indset = Set.Make(InductiveOrdered) +module Indset_env = Set.Make(InductiveOrdered_env) module Indmap = Map.Make(InductiveOrdered) module Indmap_env = Map.Make(InductiveOrdered_env) @@ -688,6 +689,8 @@ module ConstructorOrdered_env = struct let compare = constructor_user_ord end +module Constrset = Set.Make(ConstructorOrdered) +module Constrset_env = Set.Make(ConstructorOrdered_env) module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) diff --git a/kernel/names.mli b/kernel/names.mli index 78eb9295d4..0c92a2f2bc 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -471,7 +471,7 @@ end module Mindset : CSig.SetS with type elt = MutInd.t module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset -module Mindmap_env : CSig.MapS with type key = MutInd.t +module Mindmap_env : CMap.ExtS with type key = MutInd.t (** Designation of a (particular) inductive type. *) type inductive = MutInd.t (* the name of the inductive type *) @@ -484,11 +484,14 @@ type constructor = inductive (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *) -module Indset : CSig.SetS with type elt = inductive -module Indmap : CSig.MapS with type key = inductive -module Constrmap : CSig.MapS with type key = constructor -module Indmap_env : CSig.MapS with type key = inductive -module Constrmap_env : CSig.MapS with type key = constructor +module Indset : CSet.S with type elt = inductive +module Constrset : CSet.S with type elt = constructor +module Indset_env : CSet.S with type elt = inductive +module Constrset_env : CSet.S with type elt = constructor +module Indmap : CMap.ExtS with type key = inductive and module Set := Indset +module Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset +module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset_env +module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env val ind_modpath : inductive -> ModPath.t val constr_modpath : constructor -> ModPath.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 00559206ee..e846b17aa0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -302,8 +302,8 @@ let lift_constant c = let push_private_constants env eff = let eff = side_effects_of_private_constants eff in let add_if_undefined env eff = - try ignore(Environ.lookup_constant eff.seff_constant env); env - with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env + if Environ.mem_constant eff.seff_constant env then env + else Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env in List.fold_left add_if_undefined env eff @@ -598,8 +598,8 @@ let inline_side_effects env body side_eff = (** First step: remove the constants that are still in the environment *) let filter e = let cb = (e.seff_constant, e.seff_body) in - try ignore (Environ.lookup_constant e.seff_constant env); None - with Not_found -> Some (cb, e.from_env) + if Environ.mem_constant e.seff_constant env then None + else Some (cb, e.from_env) in (* CAVEAT: we assure that most recent effects come first *) let side_eff = List.map_filter filter (SideEffects.repr side_eff) in @@ -750,9 +750,7 @@ let translate_direct_opaque env kn ce = { cb with const_body = OpaqueDef c } let export_side_effects mb env (b_ctx, eff) = - let not_exists e = - try ignore(Environ.lookup_constant e.seff_constant env); false - with Not_found -> true in + let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl else e :: acc, e.from_env :: sl in diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index a43549f6c3..0a6c3afd0d 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -620,18 +620,16 @@ let lookup_eliminator env ind_sp s = let knc = KerName.make mpc l in (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) - try - let cst = Constant.make knu knc in - let _ = lookup_constant cst env in - GlobRef.ConstRef cst - with Not_found -> - (* Then try to get a user-defined eliminator in some other places *) - (* using short name (e.g. for "eq_rec") *) - try Nametab.locate (qualid_of_ident id) - with Not_found -> - user_err ~hdr:"default_elim" - (strbrk "Cannot find the elimination combinator " ++ - Id.print id ++ strbrk ", the elimination of the inductive definition " ++ - Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++ - strbrk " on sort " ++ Sorts.pr_sort_family s ++ - strbrk " is probably not allowed.") + let cst = Constant.make knu knc in + if mem_constant cst env then GlobRef.ConstRef cst + else + (* Then try to get a user-defined eliminator in some other places *) + (* using short name (e.g. for "eq_rec") *) + try Nametab.locate (qualid_of_ident id) + with Not_found -> + user_err ~hdr:"default_elim" + (strbrk "Cannot find the elimination combinator " ++ + Id.print id ++ strbrk ", the elimination of the inductive definition " ++ + Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++ + strbrk " on sort " ++ Sorts.pr_sort_family s ++ + strbrk " is probably not allowed.") diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 866c0da555..e8a2189611 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -241,8 +241,10 @@ let invert_name labs l {binder_name=na0} env sigma ref na = let refi = match ref with | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) - | EvalConst kn -> - Some (EvalConst (Constant.change_label kn (Label.of_id id))) in + | EvalConst kn -> + let kn = Constant.change_label kn (Label.of_id id) in + if Environ.mem_constant kn env then Some (EvalConst kn) else None + in match refi with | None -> None | Some ref -> diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index f6fca91eea..a806ab7123 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -16,6 +16,9 @@ val write_diffs_option : string -> unit (** Returns true if the diffs option is "on" or "removed" *) val show_diffs : unit -> bool +(** Returns true if the diffs option is "removed" *) +val show_removed : unit -> bool + (** controls whether color output is enabled *) val write_color_enabled : bool -> unit diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 9b4a628871..1e18028e7b 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -8,14 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module CVars = Vars - open Util open Termops open EConstr open Evarutil -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (* tactical to save as name a subproof such that the generalisation of @@ -39,54 +36,6 @@ let interpretable_as_section_decl env sigma d1 d2 = e_eq_constr_univs sigma b1 b2 && e_eq_constr_univs sigma t1 t2 | LocalAssum (_,t1), d2 -> e_eq_constr_univs sigma t1 (NamedDecl.get_type d2) -let rec decompose len c t accu = - let open Constr in - let open Context.Rel.Declaration in - if len = 0 then (c, t, accu) - else match kind c, kind t with - | Lambda (na, u, c), Prod (_, _, t) -> - decompose (pred len) c t (LocalAssum (na, u) :: accu) - | LetIn (na, b, u, c), LetIn (_, _, _, t) -> - decompose (pred len) c t (LocalDef (na, b, u) :: accu) - | _ -> assert false - -let rec shrink ctx sign c t accu = - let open Constr in - let open CVars in - match ctx, sign with - | [], [] -> (c, t, accu) - | p :: ctx, decl :: sign -> - if noccurn 1 c && noccurn 1 t then - let c = subst1 mkProp c in - let t = subst1 mkProp t in - shrink ctx sign c t accu - else - let c = Term.mkLambda_or_LetIn p c in - let t = Term.mkProd_or_LetIn p t in - let accu = if RelDecl.is_local_assum p - then mkVar (NamedDecl.get_id decl) :: accu - else accu - in - shrink ctx sign c t accu -| _ -> assert false - -let shrink_entry sign const = - let open Declare in - let typ = match const.proof_entry_type with - | None -> assert false - | Some t -> t - in - (* The body has been forced by the call to [build_constant_by_tactic] *) - let () = assert (Future.is_over const.proof_entry_body) in - let ((body, uctx), eff) = Future.force const.proof_entry_body in - let (body, typ, ctx) = decompose (List.length sign) body typ [] in - let (body, typ, args) = shrink ctx sign body typ [] in - let const = { const with - proof_entry_body = Future.from_val ((body, uctx), eff); - proof_entry_type = Some typ; - } in - (const, args) - let name_op_to_name ~name_op ~name suffix = match name_op with | Some s -> s @@ -103,9 +52,10 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = redundancy on constant declaration. This opens up an interesting question, how does abstract behave when discharge is local for example? *) - let suffix = if opaque - then "_subproof" - else "_subterm" in + let suffix, kind = if opaque + then "_subproof", Decls.(IsProof Lemma) + else "_subterm", Decls.(IsDefinition Definition) + in let name = name_op_to_name ~name_op ~name suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -141,7 +91,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in let ectx = Evd.evar_universe_context sigma in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly 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 @@ -152,16 +102,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let body, effs = Future.force const.Declare.proof_entry_body in (* We drop the side-effects from the entry, they already exist in the ambient environment *) - let const = { const with Declare.proof_entry_body = Future.from_val (body, ()) } in - let const, args = shrink_entry sign const in + let const = Declare.Internal.map_entry_body const ~f:(fun _ -> body, ()) in + (* EJGA: Hack related to the above call to + `build_constant_by_tactic` with `~opaque:Transparent`. Even if + the abstracted term is destined to be opaque, if we trigger the + `if poly && opaque && private_poly_univs ()` in `Proof_global` + kernel will boom. This deserves more investigation. *) + let const = Declare.Internal.set_opacity ~opaque const in + let const, args = Declare.Internal.shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = { const with Declare.proof_entry_opaque = opaque } in - let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd + Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind const in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Declare.proof_entry_universes with diff --git a/tactics/abstract.mli b/tactics/abstract.mli index 96ddbea7b2..779e46cd49 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -20,11 +20,3 @@ val cache_term_by_tactic_then -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic - -(* Internal but used in a few places; should likely be made intro a - proper library function, or incorporated into the generic constant - save path *) -val shrink_entry - : ('a, 'b) Context.Named.Declaration.pt list - -> 'c Declare.proof_entry - -> 'c Declare.proof_entry * Constr.t list diff --git a/tactics/declare.ml b/tactics/declare.ml index 57eeddb847..9f104590e7 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -174,6 +174,7 @@ let record_aux env s_ty s_bo = Aux_file.record_in_aux "context_used" v let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty + let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); @@ -184,6 +185,26 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types proof_entry_feedback = None; proof_entry_inline_code = inline} +let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types + ?(univs=default_univ_entry) body = + { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ()); + proof_entry_secctx = None; + proof_entry_type = types; + proof_entry_universes = univs; + proof_entry_opaque = opaque; + proof_entry_feedback = None; + proof_entry_inline_code = inline} + +let delayed_definition_entry ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?(univs=default_univ_entry) ?types body = + { proof_entry_body = body + ; proof_entry_secctx = section_vars + ; proof_entry_type = types + ; proof_entry_universes = univs + ; proof_entry_opaque = opaque + ; proof_entry_feedback = feedback_id + ; proof_entry_inline_code = inline + } + let cast_proof_entry e = let (body, ctx), () = Future.force e.proof_entry_body in let univs = @@ -326,6 +347,12 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff +let inline_private_constants ~univs env ce = + let body, eff = Future.force ce.proof_entry_body in + let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in + cb, univs + (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry @@ -413,3 +440,64 @@ let assumption_message id = the type of the object than to the name of the object (see discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") + +module Internal = struct + + let map_entry_body ~f entry = + { entry with proof_entry_body = Future.chain entry.proof_entry_body f } + + let map_entry_type ~f entry = + { entry with proof_entry_type = f entry.proof_entry_type } + + let set_opacity ~opaque entry = + { entry with proof_entry_opaque = opaque } + + let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body + + let rec decompose len c t accu = + let open Constr in + let open Context.Rel.Declaration in + if len = 0 then (c, t, accu) + else match kind c, kind t with + | Lambda (na, u, c), Prod (_, _, t) -> + decompose (pred len) c t (LocalAssum (na, u) :: accu) + | LetIn (na, b, u, c), LetIn (_, _, _, t) -> + decompose (pred len) c t (LocalDef (na, b, u) :: accu) + | _ -> assert false + + let rec shrink ctx sign c t accu = + let open Constr in + let open Vars in + match ctx, sign with + | [], [] -> (c, t, accu) + | p :: ctx, decl :: sign -> + if noccurn 1 c && noccurn 1 t then + let c = subst1 mkProp c in + let t = subst1 mkProp t in + shrink ctx sign c t accu + else + let c = Term.mkLambda_or_LetIn p c in + let t = Term.mkProd_or_LetIn p t in + let accu = if Context.Rel.Declaration.is_local_assum p + then mkVar (NamedDecl.get_id decl) :: accu + else accu + in + shrink ctx sign c t accu + | _ -> assert false + + let shrink_entry sign const = + let typ = match const.proof_entry_type with + | None -> assert false + | Some t -> t + in + (* The body has been forced by the call to [build_constant_by_tactic] *) + let () = assert (Future.is_over const.proof_entry_body) in + let ((body, uctx), eff) = Future.force const.proof_entry_body in + let (body, typ, ctx) = decompose (List.length sign) body typ [] in + let (body, typ, args) = shrink ctx sign body typ [] in + { const with + proof_entry_body = Future.from_val ((body, uctx), eff) + ; proof_entry_type = Some typ + }, args + +end diff --git a/tactics/declare.mli b/tactics/declare.mli index 1a037ef937..a4d3f17594 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -20,7 +20,7 @@ open Entries [Nametab] and [Impargs]. *) (** Proof entries *) -type 'a proof_entry = { +type 'a proof_entry = private { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) proof_entry_secctx : Id.Set.t option; @@ -55,10 +55,35 @@ val declare_variable i.e. Definition/Theorem/Axiom/Parameter/... *) (* Default definition entries, transparent with no secctx or proj information *) -val definition_entry : ?fix_exn:Future.fix_exn -> - ?opaque:bool -> ?inline:bool -> ?types:types -> - ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry +val definition_entry + : ?fix_exn:Future.fix_exn + -> ?opaque:bool + -> ?inline:bool + -> ?types:types + -> ?univs:Entries.universes_entry + -> ?eff:Evd.side_effects + -> constr + -> Evd.side_effects proof_entry + +val pure_definition_entry + : ?fix_exn:Future.fix_exn + -> ?opaque:bool + -> ?inline:bool + -> ?types:types + -> ?univs:Entries.universes_entry + -> constr + -> unit proof_entry + +(* Delayed definition entries *) +val delayed_definition_entry + : ?opaque:bool + -> ?inline:bool + -> ?feedback_id:Stateid.t + -> ?section_vars:Id.Set.t + -> ?univs:Entries.universes_entry + -> ?types:types + -> 'a Entries.const_entry_body + -> 'a proof_entry type import_status = ImportDefaultBehavior | ImportNeedQualified @@ -83,6 +108,15 @@ val declare_private_constant -> unit proof_entry -> Constant.t * Evd.side_effects +(** [inline_private_constants ~sideff ~univs env ce] will inline the + constants in [ce]'s body and return the body plus the updated + [UState.t]. *) +val inline_private_constants + : univs:UState.t + -> Environ.env + -> Evd.side_effects proof_entry + -> Constr.t * UState.t + (** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : @@ -101,3 +135,19 @@ val check_exists : Id.t -> unit (* Used outside this module only in indschemes *) exception AlreadyDeclared of (string option * Id.t) + +(* For legacy support, do not use *) +module Internal : sig + + val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry + val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry + (* Overriding opacity is indeed really hacky *) + val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry + + (* TODO: This is only used in DeclareDef to forward the fix to + hooks, should eventually go away *) + val get_fix_exn : 'a proof_entry -> Future.fix_exn + + val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list + +end diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 3f824a94bf..ac98b5f116 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -124,16 +124,7 @@ let define internal role id c poly univs = let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in - let entry = { - Declare.proof_entry_body = - Future.from_val ((c,Univ.ContextSet.empty), ()); - proof_entry_secctx = None; - proof_entry_type = None; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - } in + let entry = Declare.pure_definition_entry ~univs c in let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in let () = match internal with | InternalTacticRequest -> () diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 413c6540a3..3c9803432a 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -55,8 +55,7 @@ let get_current_goal_context pf = let env = Global.env () in Evd.from_env env, env -let get_current_context pf = - let p = Proof_global.get_proof pf in +let get_proof_context p = try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -64,6 +63,10 @@ let get_current_context pf = let { Proof.sigma } = Proof.data p in sigma, Global.env () +let get_current_context pf = + let p = Proof_global.get_proof pf in + get_proof_context p + let solve ?with_end_tac gi info_lvl tac pr = let tac = match with_end_tac with | None -> tac @@ -114,14 +117,14 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic ~name ctx sign ~poly typ tac = +let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~poly typ tac = let evd = Evd.from_ctx ctx in let goals = [ (Global.env_of_context sign , typ) ] in let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in try let pf, status = by tac pf in let open Proof_global in - let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in + let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> entry, status, universes @@ -135,12 +138,13 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let body, eff = Future.force ce.Declare.proof_entry_body in - let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) - else body + let cb, univs = + if side_eff then Declare.inline_private_constants ~univs env ce + else + (* GG: side effects won't get reset: no need to treat their universes specially *) + let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in + cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx in - let univs = UState.merge ~sideff:side_eff Evd.univ_rigid univs ctx in cb, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index 30514191fa..a2e742c0d7 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -27,6 +27,10 @@ val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env (** [get_current_goal_context ()] works as [get_goal_context 1] *) val get_current_goal_context : Proof_global.t -> Evd.evar_map * env +(** [get_proof_context ()] gets the goal context for the first subgoal + of the proof *) +val get_proof_context : Proof.t -> Evd.evar_map * env + (** [get_current_context ()] returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. @@ -59,6 +63,7 @@ val use_unification_heuristics : unit -> bool val build_constant_by_tactic : name:Id.t + -> ?opaque:Proof_global.opacity_flag -> UState.t -> named_context_val -> poly:bool diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index b723922642..b1fd34e43c 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -238,18 +238,10 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in - let open Declare in - { - proof_entry_body = body; - proof_entry_secctx = section_vars; - proof_entry_feedback = feedback_id; - proof_entry_type = Some typ; - proof_entry_inline_code = false; - proof_entry_opaque = opaque; - proof_entry_universes = univs; } + Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body in - let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in - { name; entries = entries; poly; universes; udecl } + let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in + { name; entries; poly; universes; udecl } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/test-suite/bugs/closed/bug_9114.v b/test-suite/bugs/closed/bug_9114.v new file mode 100644 index 0000000000..2cf91c1c2b --- /dev/null +++ b/test-suite/bugs/closed/bug_9114.v @@ -0,0 +1,5 @@ +Goal True. + assert_succeeds (exact I). + idtac. + (* Error: No such goal. *) +Abort. diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out new file mode 100644 index 0000000000..285a3bcd89 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.out @@ -0,0 +1,42 @@ +
+Coq < Coq < 1 subgoal
+
+ ============================
+ [48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
+
+x <
+x < 1 focused subgoal
+(shelved: 1)
+ [48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
+ ============================
+ [48;2;0;91;0m[37mexists[39m k : nat[37m,[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m /\[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m =[39m k[37m /\[39m i[37m =[39m k[0m
+
+[48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
+ [48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
+
+x < 1 focused subgoal
+(shelved: 2)
+ i : nat
+ ============================
+ [48;2;0;91;0mi[37m =[39m ?j[37m /\[39m ?j[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[37m /\[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
+
+x < 2 focused subgoals
+(shelved: 2)
+ i : nat
+ ============================
+ [48;2;0;91;0mi[37m =[39m ?j[0m
+
+subgoal 2 is:
+ [48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m?j[49m
+ [48;2;0;91;0m(ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m ?j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m?k [48;2;0;141;0;4m(conj[48;2;0;91;0;24m ?Goal [48;2;0;141;0;4m[94m?[39m[94mGoal0[39m)[48;2;0;91;0;24m))[0m
+
+x <
diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v new file mode 100644 index 0000000000..4251c52cb4 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.v @@ -0,0 +1,6 @@ +(* coq-prog-args: ("-color" "on" "-diffs" "on") *) +Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k. +Proof using. + eexists. Show Proof Diffs. + eexists. Show Proof Diffs. + split. Show Proof Diffs. diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 19c9fc4423..70427220ed 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -6,3 +6,4 @@ The command has indeed failed with message: H is already used. The command has indeed failed with message: H is already used. +a diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index fa12f09a46..96b6d652c9 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -22,3 +22,11 @@ intros H. Fail intros [H%myid ?]. Fail destruct 1 as [H%myid ?]. Abort. + + +(* Test that assert_succeeds only runs a tactic once *) +Ltac should_not_loop := idtac + should_not_loop. +Goal True. + assert_succeeds should_not_loop. + assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *) +Abort. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index ad6f1765a3..6de9f8f88d 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -325,9 +325,9 @@ Ltac time_constr tac := (** Useful combinators *) Ltac assert_fails tac := - tryif tac then fail 0 tac "succeeds" else idtac. + tryif (once tac) then gfail 0 tac "succeeds" else idtac. Ltac assert_succeeds tac := - tryif (assert_fails tac) then fail 0 tac "fails" else idtac. + tryif (assert_fails tac) then gfail 0 tac "fails" else idtac. Tactic Notation "assert_succeeds" tactic3(tac) := assert_succeeds tac. Tactic Notation "assert_fails" tactic3(tac) := diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 1f319d2bfd..97f0e57d2e 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -418,6 +418,50 @@ let rec vernac_loop ~state = Feedback.msg_notice (v 0 (goal ++ evars)); vernac_loop ~state + | Some VernacShowProofDiffs removed -> + (* extension of Vernacentries.show_proof *) + let to_pp pstate = + let p = Option.get pstate in + let sigma, env = Pfedit.get_proof_context p in + let pprf = Proof.partial_proof p in + Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf + (* We print nothing if there are no goals left *) + in + + if not (Proof_diffs.color_enabled ()) then + CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") + else begin + let out = + try + let n_pp = to_pp state.proof in + if true (*Proof_diffs.show_diffs ()*) then + let doc = state.doc in + let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in + try + let o_pp = to_pp oproof in + let tokenize_string = Proof_diffs.tokenize_string in + let show_removed = Some removed in + Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp + with + | Pfedit.NoSuchGoal + | Option.IsNone -> n_pp + | Pp_diff.Diff_Failure msg -> begin + (* todo: print the unparsable string (if we know it) *) + Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut() + ++ str "Showing results without diff highlighting" ); + n_pp + end + else + n_pp + with + | Pfedit.NoSuchGoal + | Option.IsNone -> + CErrors.user_err (str "No goals to show.") + in + Feedback.msg_notice out; + end; + vernac_loop ~state + | None -> top_stderr (fnl ()); exit 0 diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index e180d9e750..56fda58a25 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -22,6 +22,7 @@ type vernac_toplevel = | VernacQuit | VernacControl of vernac_control | VernacShowGoal of { gid : int; sid: int } + | VernacShowProofDiffs of bool module Toplevel_ : sig val vernac_toplevel : vernac_toplevel option Entry.t @@ -59,6 +60,8 @@ GRAMMAR EXTEND Gram (* show a goal for the specified proof state *) | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." -> { Some (VernacShowGoal {gid; sid}) } + | IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." -> + { Some (VernacShowProofDiffs (removed <> None)) } | cmd = Pvernac.Vernac_.main_entry -> { match cmd with | None -> None diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index cb034bdff6..dacef1cb18 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -135,11 +135,13 @@ let lookup_constant_in_impl cst fallback = | None -> anomaly (str "Print Assumption: unknown constant " ++ Constant.print cst ++ str ".") let lookup_constant cst = - try - let cb = Global.lookup_constant cst in + let env = Global.env() in + if not (Environ.mem_constant cst env) + then lookup_constant_in_impl cst None + else + let cb = Environ.lookup_constant cst env in if Declareops.constant_has_body cb then cb else lookup_constant_in_impl cst (Some cb) - with Not_found -> lookup_constant_in_impl cst None let lookup_mind_in_impl mind = try @@ -150,8 +152,9 @@ let lookup_mind_in_impl mind = anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind ++ str ".") let lookup_mind mind = - try Global.lookup_mind mind - with Not_found -> lookup_mind_in_impl mind + let env = Global.env() in + if Environ.mem_mind mind env then Environ.lookup_mind mind env + else lookup_mind_in_impl mind (** Graph traversal of an object, collecting on the way the dependencies of traversed objects *) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index f044c025d8..e57c324c9a 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -44,7 +44,7 @@ end (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = - let fix_exn = Future.fix_exn_of ce.proof_entry_body in + let fix_exn = Declare.Internal.get_fix_exn ce in let gr = match scope with | Discharge -> let () = diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index d6001f5970..1bb6620886 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -62,11 +62,16 @@ val declare_fix -> Impargs.manual_implicits -> GlobRef.t -val prepare_definition : allow_evars:bool -> - ?opaque:bool -> ?inline:bool -> poly:bool -> - Evd.evar_map -> UState.universe_decl -> - types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Declare.proof_entry +val prepare_definition + : allow_evars:bool + -> ?opaque:bool + -> ?inline:bool + -> poly:bool + -> Evd.evar_map + -> UState.universe_decl + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map * Evd.side_effects Declare.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 2c56f707f1..b56b9c8ce2 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -490,10 +490,8 @@ let obligation_terminator entries uctx { name; num; auto } = | [entry] -> let env = Global.env () in let ty = entry.Declare.proof_entry_type in - let body, eff = Future.force entry.Declare.proof_entry_body in - let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let body, uctx = Declare.inline_private_constants ~univs:uctx env entry in let sigma = Evd.from_ctx uctx in - let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (* Declare the obligation ourselves and drop the hook *) let prg = CEphemeron.get (ProgMap.find name !from_prg) in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 5ace8b917c..7010aa8c6d 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -384,17 +384,14 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - { const with - Declare.proof_entry_body = - Future.chain const.Declare.proof_entry_body - (fun ((body, ctx), eff) -> - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = search_guard env possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) - } + Declare.Internal.map_entry_body const + ~f:(fun ((body, ctx), eff) -> + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff) let finish_proved env sigma idopt po info = let open Proof_global in @@ -404,7 +401,7 @@ let finish_proved env sigma idopt po info = let name = match idopt with | None -> name | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in - let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in + let fix_exn = Declare.Internal.get_fix_exn const in let () = try let const = adjust_guardness_conditions const compute_guard in let should_suggest = const.Declare.proof_entry_opaque && @@ -452,7 +449,7 @@ let finish_derived ~f ~name ~idopt ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Declare.proof_entry_opaque = false } in + let f_def = Declare.Internal.set_opacity ~opaque:false f_def in let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in @@ -463,20 +460,15 @@ let finish_derived ~f ~name ~idopt ~entries = performs this precise action. *) let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype = - match lemma_def.Declare.proof_entry_type with - | Some t -> t + let lemma_pretype typ = + match typ with + | Some t -> Some (substf t) | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) - let lemma_type = substf lemma_pretype in + let lemma_def = Declare.Internal.map_entry_type lemma_def ~f:lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = - { lemma_def with - Declare.proof_entry_body = lemma_body; - proof_entry_type = Some lemma_type } - in + let lemma_def = Declare.Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in let lemma_def = Declare.DefinitionEntry lemma_def in let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in () @@ -491,7 +483,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = | Some id -> id | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) in - let entry, args = Abstract.shrink_entry local_context entry in + let entry, args = Declare.Internal.shrink_entry local_context entry in let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c8cede1f84..4ea34e2b60 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -423,11 +423,9 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.Declare.proof_entry_body in - let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in - let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in - Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx') + let body, ctx' = Declare.inline_private_constants ~univs:ctx' env entry in + Inductiveops.control_only_guard env (Evd.from_ctx ctx') (EConstr.of_constr body); + Some (body, entry.Declare.proof_entry_type, ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in |