aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/btermdn.ml2
-rw-r--r--tactics/class_tactics.ml4
-rw-r--r--tactics/elimschemes.ml4
-rw-r--r--tactics/hints.ml46
-rw-r--r--tactics/hints.mli39
-rw-r--r--tactics/hipattern.ml6
-rw-r--r--tactics/hipattern.mli2
-rw-r--r--tactics/tacticals.ml12
-rw-r--r--tactics/tacticals.mli6
-rw-r--r--tactics/tactics.ml63
-rw-r--r--tactics/tactics.mli5
-rw-r--r--tactics/term_dnet.ml2
12 files changed, 110 insertions, 81 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 8e50c977e7..8f50b0aa23 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -22,7 +22,7 @@ open Globnames
let dnet_depth = ref 8
type term_label =
-| GRLabel of global_reference
+| GRLabel of GlobRef.t
| ProdLabel
| LambdaLabel
| SortLabel
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b11e36bceb..bbcf8def6d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -547,9 +547,9 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
(List.map_append
(fun (path,info,c) ->
let info =
- { info with Vernacexpr.hint_pattern =
+ { info with hint_pattern =
Option.map (Constrintern.intern_constr_pattern env sigma)
- info.Vernacexpr.hint_pattern }
+ info.hint_pattern }
in
make_resolves env sigma ~name:(PathHints path)
(true,false,not !Flags.quiet) info false
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 6bd4866c61..70f73df5c1 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -46,8 +46,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
mib.mind_nparams in
let sigma, sort = Evd.fresh_sort_in_family env sigma sort in
let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
- let sigma, nf = Evarutil.nf_evars_and_universes sigma in
- (nf c', Evd.evar_universe_context sigma), eff
+ let sigma = Evd.minimize_universes sigma in
+ (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff
else
let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
let sigma, c = build_induction_scheme env sigma pind dep sort in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 46d1629119..d02bab1864 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -28,12 +28,13 @@ open Termops
open Inductiveops
open Typing
open Decl_kinds
+open Vernacexpr
+open Typeclasses
open Pattern
open Patternops
open Clenv
open Tacred
open Printer
-open Vernacexpr
module NamedDecl = Context.Named.Declaration
@@ -94,7 +95,6 @@ let secvars_of_hyps hyps =
else pred
let empty_hint_info =
- let open Vernacexpr in
{ hint_priority = None; hint_pattern = None }
(************************************************************************)
@@ -115,7 +115,7 @@ type 'a hints_path_atom_gen =
(* For forward hints, their names is the list of projections *)
| PathAny
-type hints_path_atom = global_reference hints_path_atom_gen
+type hints_path_atom = GlobRef.t hints_path_atom_gen
type 'a hints_path_gen =
| PathAtom of 'a hints_path_atom_gen
@@ -126,10 +126,10 @@ type 'a hints_path_gen =
| PathEpsilon
type pre_hints_path = Libnames.reference hints_path_gen
-type hints_path = global_reference hints_path_gen
+type hints_path = GlobRef.t hints_path_gen
type hint_term =
- | IsGlobRef of global_reference
+ | IsGlobRef of GlobRef.t
| IsConstr of constr * Univ.ContextSet.t
type 'a with_uid = {
@@ -153,7 +153,7 @@ type 'a with_metadata = {
type full_hint = hint with_metadata
-type hint_entry = global_reference option *
+type hint_entry = GlobRef.t option *
raw_hint hint_ast with_uid with_metadata
type import_level = [ `LAX | `WARN | `STRICT ]
@@ -308,7 +308,7 @@ let instantiate_hint env sigma p =
{ p with code = { p.code with obj = code } }
let hints_path_atom_eq h1 h2 = match h1, h2 with
-| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2
+| PathHints l1, PathHints l2 -> List.equal GlobRef.equal l1 l2
| PathAny, PathAny -> true
| _ -> false
@@ -365,7 +365,7 @@ let path_seq p p' =
let rec path_derivate hp hint =
let rec derivate_atoms hints hints' =
match hints, hints' with
- | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs'
+ | gr :: grs, gr' :: grs' when GlobRef.equal gr gr' -> derivate_atoms grs grs'
| [], [] -> PathEpsilon
| [], hints -> PathEmpty
| grs, [] -> PathAtom (PathHints grs)
@@ -474,28 +474,28 @@ module Hint_db :
sig
type t
val empty : ?name:hint_db_name -> transparent_state -> bool -> t
-val find : global_reference -> t -> search_entry
+val find : GlobRef.t -> t -> search_entry
val map_none : secvars:Id.Pred.t -> t -> full_hint list
-val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
val map_existential : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val map_eauto : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val map_auto : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val add_one : env -> evar_map -> hint_entry -> t -> t
val add_list : env -> evar_map -> hint_entry list -> t -> t
-val remove_one : global_reference -> t -> t
-val remove_list : global_reference list -> t -> t
-val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
+val remove_one : GlobRef.t -> t -> t
+val remove_list : GlobRef.t list -> t -> t
+val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
val transparent_state : t -> transparent_state
val set_transparent_state : t -> transparent_state -> t
val add_cut : hints_path -> t -> t
-val add_mode : global_reference -> hint_mode array -> t -> t
+val add_mode : GlobRef.t -> hint_mode array -> t -> t
val cut : t -> hints_path
val unfolds : t -> Id.Set.t * Cset.t
-val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
+val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
t -> 'a -> 'a
end =
@@ -510,7 +510,7 @@ struct
hintdb_map : search_entry Constr_map.t;
(* A list of unindexed entries starting with an unfoldable constant
or with no associated pattern. *)
- hintdb_nopat : (global_reference option * stored_data) list;
+ hintdb_nopat : (GlobRef.t option * stored_data) list;
hintdb_name : string option;
}
@@ -664,7 +664,7 @@ struct
let remove_list grs db =
let filter (_, h) =
- match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in
+ match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
{ db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
@@ -1015,9 +1015,9 @@ type hint_action =
| CreateDB of bool * transparent_state
| AddTransparency of evaluable_global_reference list * bool
| AddHints of hint_entry list
- | RemoveHints of global_reference list
+ | RemoveHints of GlobRef.t list
| AddCut of hints_path
- | AddMode of global_reference * hint_mode array
+ | AddMode of GlobRef.t * hint_mode array
let add_cut dbname path =
let db = get_db dbname in
@@ -1226,7 +1226,7 @@ type hints_entry =
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
- | HintsModeEntry of global_reference * hint_mode list
+ | HintsModeEntry of GlobRef.t * hint_mode list
| HintsExternEntry of hint_info * Genarg.glob_generic_argument
let default_prepare_hint_ident = Id.of_string "H"
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 1811150c2a..c7de10a2a5 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -12,7 +12,6 @@ open Util
open Names
open EConstr
open Environ
-open Globnames
open Decl_kinds
open Evd
open Misctypes
@@ -25,13 +24,13 @@ open Vernacexpr
exception Bound
-val decompose_app_bound : evar_map -> constr -> global_reference * constr array
+val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array
type debug = Debug | Info | Off
val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t
-val empty_hint_info : 'a hint_info_gen
+val empty_hint_info : 'a Typeclasses.hint_info_gen
(** Pre-created hint databases *)
@@ -51,7 +50,7 @@ type 'a hints_path_atom_gen =
(* For forward hints, their names is the list of projections *)
| PathAny
-type hints_path_atom = global_reference hints_path_atom_gen
+type hints_path_atom = GlobRef.t hints_path_atom_gen
type hint_db_name = string
type 'a with_metadata = private {
@@ -81,7 +80,7 @@ type 'a hints_path_gen =
| PathEpsilon
type pre_hints_path = Libnames.reference hints_path_gen
-type hints_path = global_reference hints_path_gen
+type hints_path = GlobRef.t hints_path_gen
val normalize_path : hints_path -> hints_path
val path_matches : hints_path -> hints_path_atom list -> bool
@@ -91,15 +90,15 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
val pp_hints_path : hints_path -> Pp.t
val pp_hint_mode : hint_mode -> Pp.t
val glob_hints_path_atom :
- Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
+ Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
val glob_hints_path :
- Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen
+ Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen
module Hint_db :
sig
type t
val empty : ?name:hint_db_name -> transparent_state -> bool -> t
- val find : global_reference -> t -> search_entry
+ val find : GlobRef.t -> t -> search_entry
(** All hints which have no pattern.
* [secvars] represent the set of section variables that
@@ -107,27 +106,27 @@ module Hint_db :
val map_none : secvars:Id.Pred.t -> t -> full_hint list
(** All hints associated to the reference *)
- val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+ val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments, _not_ using the discrimination net. *)
val map_existential : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments and using the discrimination net. *)
- val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list
+ val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments. *)
val map_auto : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val add_one : env -> evar_map -> hint_entry -> t -> t
val add_list : env -> evar_map -> hint_entry list -> t -> t
- val remove_one : global_reference -> t -> t
- val remove_list : global_reference list -> t -> t
- val iter : (global_reference option ->
+ val remove_one : GlobRef.t -> t -> t
+ val remove_list : GlobRef.t list -> t -> t
+ val iter : (GlobRef.t option ->
hint_mode array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
@@ -144,10 +143,10 @@ type hint_db = Hint_db.t
type hnf = bool
-type hint_info = (patvar list * constr_pattern) hint_info_gen
+type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen
type hint_term =
- | IsGlobRef of global_reference
+ | IsGlobRef of GlobRef.t
| IsConstr of constr * Univ.ContextSet.t
type hints_entry =
@@ -157,7 +156,7 @@ type hints_entry =
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
- | HintsModeEntry of global_reference * hint_mode list
+ | HintsModeEntry of GlobRef.t * hint_mode list
| HintsExternEntry of hint_info * Genarg.glob_generic_argument
val searchtable_map : hint_db_name -> hint_db
@@ -171,7 +170,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit
val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
-val remove_hints : bool -> hint_db_name list -> global_reference list -> unit
+val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit
val current_db_names : unit -> String.Set.t
@@ -264,7 +263,7 @@ val rewrite_db : hint_db_name
val pr_searchtable : env -> evar_map -> Pp.t
val pr_applicable_hint : unit -> Pp.t
-val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t
+val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
val pr_hint_db : Hint_db.t -> Pp.t
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index b012a7ecd1..b8f1ed720b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -294,13 +294,13 @@ let match_with_equation env sigma t =
let (hdapp,args) = destApp sigma t in
match EConstr.kind sigma hdapp with
| Ind (ind,u) ->
- if eq_gr (IndRef ind) glob_eq then
+ if GlobRef.equal (IndRef ind) glob_eq then
Some (build_coq_eq_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if eq_gr (IndRef ind) glob_identity then
+ else if GlobRef.equal (IndRef ind) glob_identity then
Some (build_coq_identity_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if eq_gr (IndRef ind) glob_jmeq then
+ else if GlobRef.equal (IndRef ind) glob_jmeq then
Some (build_coq_jmeq_data()),hdapp,
HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
else
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 0697d0f19c..f04cda1232 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -144,7 +144,7 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool
(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
[t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
+val match_eqdec : Environ.env -> evar_map -> constr -> bool * GlobRef.t * constr * constr * constr
(** Match a negation *)
val is_matching_not : Environ.env -> evar_map -> constr -> bool
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5e81e2d4b1..6c7db26c77 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -492,11 +492,13 @@ module New = struct
Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
(* Select a subset of the goals *)
- let tclSELECT = function
- | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
- | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
- | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
- | Vernacexpr.SelectAll -> fun tac -> tac
+ let tclSELECT = let open Goal_select in function
+ | SelectNth i -> Proofview.tclFOCUS i i
+ | SelectList l -> Proofview.tclFOCUSLIST l
+ | SelectId id -> Proofview.tclFOCUSID id
+ | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
+ | SelectAlreadyFocused ->
+ anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
(* Check that holes in arguments have been resolved *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 340d8fbf3d..cbaf691f1f 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -135,7 +135,7 @@ val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family
val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family
val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
-val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
+val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic
(** Tacticals defined directly in term of Proofview *)
@@ -223,7 +223,7 @@ module New : sig
val tclCOMPLETE : 'a tactic -> 'a tactic
val tclSOLVE : unit tactic list -> unit tactic
val tclPROGRESS : unit tactic -> unit tactic
- val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic
+ val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic
val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
@@ -268,5 +268,5 @@ module New : sig
val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
- val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
+ val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aae4bc0885..ee76ad077a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -198,32 +198,40 @@ end
let convert x y = convert_gen Reduction.CONV x y
let convert_leq x y = convert_gen Reduction.CUMUL x y
-let clear_dependency_msg env sigma id = function
+let clear_in_global_msg = function
+ | None -> mt ()
+ | Some ref -> str " implicitly in " ++ Printer.pr_global ref
+
+let clear_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- Id.print id ++ str " is used in conclusion."
+ Id.print id ++ str " is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
- Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"."
+ Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot remove " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_clear_dependency env sigma id err =
- user_err (clear_dependency_msg env sigma id err)
+let error_clear_dependency env sigma id err inglobal =
+ user_err (clear_dependency_msg env sigma id err inglobal)
-let replacing_dependency_msg env sigma id = function
+let replacing_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion."
+ str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
str "Cannot change " ++ Id.print id ++
- strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"."
+ strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot change " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_replacing_dependency env sigma id err =
- user_err (replacing_dependency_msg env sigma id err)
+let error_replacing_dependency env sigma id err inglobal =
+ user_err (replacing_dependency_msg env sigma id err inglobal)
(* This tactic enables the user to remove hypotheses from the signature.
* Some care is taken to prevent him from removing variables that are
@@ -242,7 +250,7 @@ let clear_gen fail = function
let evdref = ref sigma in
let (hyps, concl) =
try clear_hyps_in_evi env evdref (named_context_val env) concl ids
- with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
+ with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal
in
let env = reset_with_named_context hyps env in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
@@ -426,8 +434,8 @@ let clear_hyps2 env sigma ids sign t cl =
let evdref = ref (Evd.clear_metas sigma) in
let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
(hyps, t, cl, !evdref)
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency env sigma id err
+ with Evarutil.ClearDependencyError (id,err,inglobal) ->
+ error_replacing_dependency env sigma id err inglobal
let internal_cut_gen ?(check=true) dir replace id t =
Proofview.Goal.enter begin fun gl ->
@@ -971,6 +979,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
| LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
let name = find_name false (LocalDef (name,b,t)) name_flag gl in
build_intro_tac name move_flag tac
+ | Evar ev when force_flag ->
+ let sigma, t = Evardefine.define_evar_as_product sigma ev in
+ Tacticals.New.tclTHEN
+ (Proofview.Unsafe.tclEVARS sigma)
+ (intro_then_gen name_flag move_flag force_flag dep_flag tac)
| _ ->
begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
(* Note: red_in_concl includes betaiotazeta and this was like *)
@@ -3007,8 +3020,24 @@ let unfold_body x =
end
end
+let warn_cannot_remove_as_expected =
+ CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics"
+ (fun (id,inglobal) ->
+ let pp = match inglobal with
+ | None -> mt ()
+ | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in
+ str "Cannot remove " ++ Id.print id ++ pp ++ str ".")
+
+let clear_for_destruct ids =
+ Proofview.tclORELSE
+ (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids)
+ (function
+ | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT ()
+ | e -> iraise e)
+
(* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
+let expand_hyp id =
+ Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id]
(*****************************)
(* High-level induction *)
@@ -3424,7 +3453,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
type elim_scheme = {
elimc: constr with_bindings option;
elimt: types;
- indref: global_reference option;
+ indref: GlobRef.t option;
params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
nparams: int; (* number of parameters *)
predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
@@ -4929,9 +4958,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
let evd, ctx, concl =
(* FIXME: should be done only if the tactic succeeds *)
- let evd, nf = nf_evars_and_universes !evdref in
+ let evd = Evd.minimize_universes !evdref in
let ctx = Evd.universe_context_set evd in
- evd, ctx, nf concl
+ evd, ctx, Evarutil.nf_evars_universes evd concl
in
let concl = EConstr.of_constr concl in
let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7809dbf480..46f782eaa5 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -16,7 +16,6 @@ open Proof_type
open Evd
open Clenv
open Redexpr
-open Globnames
open Pattern
open Unification
open Misctypes
@@ -177,7 +176,7 @@ val change :
val pattern_option :
(occurrences * constr) list -> goal_location -> unit Proofview.tactic
val reduce : red_expr -> clause -> unit Proofview.tactic
-val unfold_constr : global_reference -> unit Proofview.tactic
+val unfold_constr : GlobRef.t -> unit Proofview.tactic
(** {6 Modification of the local context. } *)
@@ -253,7 +252,7 @@ val apply_delayed_in :
type elim_scheme = {
elimc: constr with_bindings option;
elimt: types;
- indref: global_reference option;
+ indref: GlobRef.t option;
params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
nparams: int; (** number of parameters *)
predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 753c608ada..6117999902 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -37,7 +37,7 @@ struct
type 't t =
| DRel
| DSort
- | DRef of global_reference
+ | DRef of GlobRef.t
| DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *)
| DLambda of 't * 't
| DApp of 't * 't (* binary app *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 21:09:45 +0000