aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/abstract.ml49
-rw-r--r--tactics/abstract.mli8
-rw-r--r--tactics/class_tactics.ml10
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/ind_tables.ml2
-rw-r--r--tactics/leminv.ml6
-rw-r--r--tactics/tactics.ml9
7 files changed, 50 insertions, 36 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 3a687a6b41..7a61deba0c 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
@@ -147,8 +162,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
in
let cst = Impargs.with_implicit_protection cst () in
let inst = match const.Entries.const_entry_universes with
- | Entries.Monomorphic_const_entry _ -> EInstance.empty
- | Entries.Polymorphic_const_entry (_, ctx) ->
+ | Entries.Monomorphic_entry _ -> EInstance.empty
+ | Entries.Polymorphic_entry (_, ctx) ->
(* We mimick what the kernel does, that is ensuring that no additional
constraints appear in the body of polymorphic constants. Ideally this
should be enforced statically. *)
@@ -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/tactics/hints.ml b/tactics/hints.ml
index 571ad9d160..c1f6365f5d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1309,7 +1309,7 @@ let project_hint ~poly pri l2r r =
let id =
Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
in
- let ctx = Evd.const_univ_entry ~poly sigma in
+ let ctx = Evd.univ_entry ~poly sigma in
let c = EConstr.to_constr sigma c in
let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index a67f5f6d6e..d1b77f3758 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -121,7 +121,7 @@ let define internal id c poly univs =
let id = compute_name internal id in
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.const_univ_entry ~poly ctx in
+ let univs = UState.univ_entry ~poly ctx in
let entry = {
const_entry_body =
Future.from_val ((c,Univ.ContextSet.empty),
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 356b43ec14..335f3c74ff 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -237,9 +237,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
- let univs =
- Evd.const_univ_entry ~poly sigma
- in
+ let univs = Evd.univ_entry ~poly sigma in
let entry = definition_entry ~univs invProof in
let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
()
@@ -250,7 +248,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let add_inversion_lemma_exn ~poly na com comsort bool tac =
let env = Global.env () in
let sigma = Evd.from_env env in
- let sigma, c = Constrintern.interp_type_evars env sigma com in
+ let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
try
add_inversion_lemma ~poly na env sigma c sort bool tac
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 070b2356e5..db59f7cfc2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1155,7 +1155,9 @@ let tactic_infer_flags with_evar = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = true;
Pretyping.fail_evar = not with_evar;
- Pretyping.expand_evars = true }
+ Pretyping.expand_evars = true;
+ Pretyping.program_mode = false;
+}
type evars_flag = bool (* true = pose evars false = fail on evars *)
type rec_flag = bool (* true = recursive false = not recursive *)
@@ -4522,8 +4524,11 @@ let induction_gen clear_flag isrec with_evars elim
declaring the induction argument as a new local variable *)
let id =
(* Type not the right one if partially applied but anyway for internal use*)
+ let avoid = match eqname with
+ | Some {CAst.v=IntroIdentifier id} -> Id.Set.singleton id
+ | _ -> Id.Set.empty in
let x = id_of_name_using_hdchar env evd t Anonymous in
- new_fresh_id Id.Set.empty x gl in
+ new_fresh_id avoid x gl in
let info_arg = (is_arg_pure_hyp, not enough_applied) in
pose_induction_arg_then
isrec with_evars info_arg elim id arg t inhyps cls
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 21:06:21 +0000