aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml41
-rw-r--r--tactics/auto.mli2
-rw-r--r--tactics/class_tactics.ml86
-rw-r--r--tactics/eauto.ml11
-rw-r--r--tactics/equality.ml28
-rw-r--r--tactics/hints.ml59
-rw-r--r--tactics/hints.mli7
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tactics.ml42
10 files changed, 163 insertions, 119 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 962af4b5c5..6c5ecac943 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -260,31 +260,25 @@ let pr_info_atom (d,pp) =
let pr_info_trace = function
| (Info,_,{contents=(d,Some pp)::l}) ->
- prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)
- | _ -> mt ()
+ Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l))
+ | _ -> ()
let pr_info_nop = function
- | (Info,_,_) -> str "idtac."
- | _ -> mt ()
+ | (Info,_,_) -> Feedback.msg_info (str "idtac.")
+ | _ -> ()
let pr_dbg_header = function
- | (Off,_,_) -> mt ()
- | (Debug,0,_) -> str "(* debug trivial : *)"
- | (Debug,_,_) -> str "(* debug auto : *)"
- | (Info,0,_) -> str "(* info trivial : *)"
- | (Info,_,_) -> str "(* info auto : *)"
+ | (Off,_,_) -> ()
+ | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
+ | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
+ | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)")
+ | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)")
let tclTRY_dbg d tac =
- let (level, _, _) = d in
let delay f = Proofview.tclUNIT () >>= fun () -> f () in
- let tac = match level with
- | Off -> tac
- | Debug | Info -> delay (fun () -> Feedback.msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac)
- in
- let after = match level with
- | Info -> delay (fun () -> Feedback.msg_debug (pr_info_nop d); Proofview.tclUNIT ())
- | Off | Debug -> Proofview.tclUNIT ()
- in
+ let tac = delay (fun () -> pr_dbg_header d; tac) >>=
+ fun () -> pr_info_trace d; Proofview.tclUNIT () in
+ let after = delay (fun () -> pr_info_nop d; Proofview.tclUNIT ()) in
Tacticals.New.tclORELSE0 tac after
(**************************************************************************)
@@ -375,7 +369,7 @@ and my_find_search_delta db_list local_db hdc concl =
in List.map (fun x -> (Some flags,x)) l)
(local_db::db_list)
-and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) =
+and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
let tactic = function
| Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
| ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
@@ -394,7 +388,14 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
| Extern tacast ->
conclPattern concl p tacast
in
- tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic)
+ let pr_hint () =
+ let origin = match dbname with
+ | None -> mt ()
+ | Some n -> str " (in " ++ str n ++ str ")"
+ in
+ pr_hint t ++ origin
+ in
+ tclLOG dbg pr_hint (run_hint t tactic)
and trivial_resolve dbg mod_delta db_list local_db cl =
try
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 1608a0ea63..5384140c2a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -15,8 +15,6 @@ open Pattern
open Decl_kinds
open Hints
-val priority : ('a * full_hint) list -> ('a * full_hint) list
-
val default_search_depth : int ref
val auto_flags_of_state : transparent_state -> Unification.unify_flags
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 8d6c085e63..0944cbe38f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -43,7 +43,11 @@ let typeclasses_modulo_eta = ref false
let set_typeclasses_modulo_eta d = (:=) typeclasses_modulo_eta d
let get_typeclasses_modulo_eta () = !typeclasses_modulo_eta
-let typeclasses_limit_intros = ref false
+(** When this flag is enabled, the resolution of type classes tries to avoid
+ useless introductions. This is no longer useful since we have eta, but is
+ here for compatibility purposes. Another compatibility issues is that the
+ cost (in terms of search depth) can differ. *)
+let typeclasses_limit_intros = ref true
let set_typeclasses_limit_intros d = (:=) typeclasses_limit_intros d
let get_typeclasses_limit_intros () = !typeclasses_limit_intros
@@ -55,31 +59,22 @@ let typeclasses_iterative_deepening = ref false
let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d
let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening
-let get_compat_version d =
- match d with
- | "8.5" -> Flags.V8_5
- | _ -> Flags.Current
-
-let typeclasses_unif_compat = ref Flags.V8_5
-let set_typeclasses_unif_compat d =
- if d == Flags.Current then set_typeclasses_limit_intros false
- else set_typeclasses_limit_intros true;
- (:=) typeclasses_unif_compat d
-
-let get_typeclasses_unif_compat () = !typeclasses_unif_compat
-let set_typeclasses_unif_compat_string d =
- set_typeclasses_unif_compat (get_compat_version d)
-let get_typeclasses_unif_compat_string () =
- Flags.pr_version (get_typeclasses_unif_compat ())
-
-let typeclasses_compat = ref Flags.Current
-let set_typeclasses_compat d = (:=) typeclasses_compat d
-let get_typeclasses_compat () = !typeclasses_compat
-let set_typeclasses_compat_string d =
- set_typeclasses_compat (get_compat_version d)
-
-let get_typeclasses_compat_string () =
- Flags.pr_version (get_typeclasses_compat ())
+(** [typeclasses_filtered_unif] governs the unification algorithm used by type
+ classes. If enabled, a new algorithm based on pattern filtering and refine
+ will be used. When disabled, the previous algorithm based on apply will be
+ used. *)
+let typeclasses_filtered_unification = ref false
+let set_typeclasses_filtered_unification d =
+ (:=) typeclasses_filtered_unification d
+let get_typeclasses_filtered_unification () =
+ !typeclasses_filtered_unification
+
+(** [typeclasses_legacy_resolution] falls back to the 8.5 resolution algorithm,
+ instead of the 8.6 one which uses the native backtracking facilities of the
+ proof engine. *)
+let typeclasses_legacy_resolution = ref false
+let set_typeclasses_legacy_resolution d = (:=) typeclasses_legacy_resolution d
+let get_typeclasses_legacy_resolution () = !typeclasses_legacy_resolution
let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0)
let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false
@@ -133,22 +128,22 @@ let _ =
optwrite = set_typeclasses_iterative_deepening; }
let _ =
- declare_string_option
+ declare_bool_option
{ optsync = true;
optdepr = false;
optname = "compat";
- optkey = ["Typeclasses";"Compatibility"];
- optread = get_typeclasses_compat_string;
- optwrite = set_typeclasses_compat_string; }
+ optkey = ["Typeclasses";"Legacy";"Resolution"];
+ optread = get_typeclasses_legacy_resolution;
+ optwrite = set_typeclasses_legacy_resolution; }
let _ =
- declare_string_option
+ declare_bool_option
{ optsync = true;
optdepr = false;
optname = "compat";
- optkey = ["Typeclasses";"Unification";"Compatibility"];
- optread = get_typeclasses_unif_compat_string;
- optwrite = set_typeclasses_unif_compat_string; }
+ optkey = ["Typeclasses";"Filtered";"Unification"];
+ optread = get_typeclasses_filtered_unification;
+ optwrite = set_typeclasses_filtered_unification; }
let set_typeclasses_debug =
declare_bool_option
@@ -400,7 +395,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
let tac = function
| Res_pf (term,cl) ->
- if get_typeclasses_unif_compat () = Flags.Current then
+ if get_typeclasses_filtered_unification () then
let tac =
with_prods nprods poly (term,cl)
({ enter = fun gl clenv ->
@@ -410,13 +405,13 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
else
let tac =
with_prods nprods poly (term,cl) (unify_resolve poly flags) in
- if get_typeclasses_compat () = Flags.V8_5 then
+ if get_typeclasses_legacy_resolution () then
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
Proofview.tclBIND (Proofview.with_shelf tac)
(fun (gls, ()) -> shelve_dependencies gls)
| ERes_pf (term,cl) ->
- if get_typeclasses_unif_compat () = Flags.Current then
+ if get_typeclasses_filtered_unification () then
let tac = (with_prods nprods poly (term,cl)
({ enter = fun gl clenv ->
(matches_pattern concl p) <*>
@@ -425,7 +420,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
else
let tac =
with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
- if get_typeclasses_compat () = Flags.V8_5 then
+ if get_typeclasses_legacy_resolution () then
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
Proofview.tclBIND (Proofview.with_shelf tac)
@@ -445,7 +440,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
let pp =
match p with
- | Some pat when get_typeclasses_unif_compat () = Flags.Current ->
+ | Some pat when get_typeclasses_filtered_unification () ->
str " with pattern " ++ Printer.pr_constr_pattern pat
| _ -> mt ()
in
@@ -1293,7 +1288,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
in
let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in
- if get_typeclasses_compat () = Flags.V8_5 then
+ if get_typeclasses_legacy_resolution () then
Proofview.V82.tactic
(fun gl ->
try V85.eauto85 depth ~only_classes ~st dbs gl
@@ -1419,10 +1414,10 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
let p = select_and_update_evars p oevd (in_comp comp) in
try
let evd' =
- if get_typeclasses_compat () = Flags.Current then
- Search.typeclasses_resolve debug depth unique p evd
- else
+ if get_typeclasses_legacy_resolution () then
V85.resolve_all_evars_once debug depth unique p evd
+ else
+ Search.typeclasses_resolve debug depth unique p evd
in
if has_undefined p oevd evd' then raise Unresolved;
docomp evd' comps
@@ -1467,12 +1462,13 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
let st = Hint_db.transparent_state hints in
let depth = get_typeclasses_depth () in
let gls' =
- if get_typeclasses_compat () = Flags.Current then
+ if get_typeclasses_legacy_resolution () then
+ V85.eauto85 depth ~st [hints] gls
+ else
try
Proofview.V82.of_tactic
(Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls
with Refiner.FailError _ -> raise Not_found
- else V85.eauto85 depth ~st [hints] gls
in
let evd = sig_sig gls' in
let t' = let (ev, inst) = destEvar t in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index ba9a2d95c8..5ca68cbe96 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -282,7 +282,8 @@ module SearchProblem = struct
in
let rec_tacs =
let l =
- filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+ let concl = Reductionops.nf_evar (project g)(pf_concl g) in
+ filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) concl)
in
List.map
(fun (lgls, cost, pp) ->
@@ -345,13 +346,13 @@ let mk_eauto_dbg d =
else Off
let pr_info_nop = function
- | Info -> Feedback.msg_debug (str "idtac.")
+ | Info -> Feedback.msg_info (str "idtac.")
| _ -> ()
let pr_dbg_header = function
| Off -> ()
- | Debug -> Feedback.msg_debug (str "(* debug eauto : *)")
- | Info -> Feedback.msg_debug (str "(* info eauto : *)")
+ | Debug -> Feedback.msg_debug (str "(* debug eauto: *)")
+ | Info -> Feedback.msg_info (str "(* info eauto: *)")
let pr_info dbg s =
if dbg != Info then ()
@@ -362,7 +363,7 @@ let pr_info dbg s =
| State sp ->
let mindepth = loop sp in
let indent = String.make (mindepth - sp.depth) ' ' in
- Feedback.msg_debug (str indent ++ Lazy.force s.last_tactic ++ str ".");
+ Feedback.msg_info (str indent ++ Lazy.force s.last_tactic ++ str ".");
mindepth
in
ignore (loop s)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3e5b7b65ff..e9d08d7375 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -701,16 +701,16 @@ let replace_in_clause_maybe_by c1 c2 cl tac_opt =
exception DiscrFound of
(constructor * int) list * constructor * constructor
-let injection_on_proofs = ref false
+let keep_proof_equalities_for_injection = ref false
let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
optname = "injection on prop arguments";
- optkey = ["Injection";"On";"Proofs"];
- optread = (fun () -> !injection_on_proofs) ;
- optwrite = (fun b -> injection_on_proofs := b) }
+ optkey = ["Keep";"Proof";"Equalities"];
+ optread = (fun () -> !keep_proof_equalities_for_injection) ;
+ optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
let find_positions env sigma t1 t2 =
@@ -755,7 +755,7 @@ let find_positions env sigma t1 t2 =
project env sorts posn t1_0 t2_0
in
try
- let sorts = if !injection_on_proofs then [InSet;InType;InProp]
+ let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
else [InSet;InType]
in
Inr (findrec sorts [] t1 t2)
@@ -1389,7 +1389,10 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
| Inl _ ->
tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
| Inr [] ->
- let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in
+ let suggestion =
+ if !keep_proof_equalities_for_injection then
+ "" else
+ " You can try to use option Set Keep Proof Equalities." in
tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
| Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
tclZEROMSG (str"Nothing to inject.")
@@ -1761,35 +1764,38 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let gl = Proofview.Goal.assume gl in
let env = Proofview.Goal.env gl in
let find_eq_data_decompose = find_eq_data_decompose gl in
- let test decl =
+ let select_equation_name decl =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose (get_type decl) in
let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
match kind_of_term x, kind_of_term y with
- | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
+ | Var z, _ when not (is_evaluable env (EvalVarRef z)) ->
+ Some (get_id decl)
+ | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
Some (get_id decl)
| _ ->
None
with Constr_matching.PatternMatchingFailure -> None
in
let hyps = Proofview.Goal.hyps gl in
- List.rev (List.map_filter test hyps)
+ List.rev (List.map_filter select_equation_name hyps)
in
(* Second step: treat equations *)
let process hyp =
Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
+ let env = Proofview.Goal.env gl in
let find_eq_data_decompose = find_eq_data_decompose gl in
let c = pf_get_hyp hyp gl |> get_type in
let _,_,(_,x,y) = find_eq_data_decompose c in
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if Term.eq_constr x y then Proofview.tclUNIT () else
match kind_of_term x, kind_of_term y with
- | Var x', _ when not (occur_term x y) ->
+ | Var x', _ when not (occur_term x y) && not (is_evaluable env (EvalVarRef x')) ->
subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
- | _, Var y' when not (occur_term y x) ->
+ | _, Var y' when not (occur_term y x) && not (is_evaluable env (EvalVarRef y')) ->
subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
| _ ->
Proofview.tclUNIT ()
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 8f3eb5eb51..89ecc6c0b2 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -108,6 +108,7 @@ type 'a with_metadata = {
poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *)
pat : constr_pattern option; (* A pattern for the concl of the Goal *)
name : hints_path_atom; (* A potential name to refer to the hint *)
+ db : string option; (** The database from which the hint comes *)
code : 'a; (* the tactic to apply when the concl matches pat *)
}
@@ -410,7 +411,35 @@ let rec subst_hints_path subst hp =
if p' == p && q' == q then hp else PathOr (p', q')
| _ -> hp
-module Hint_db = struct
+type hint_db_name = string
+
+module Hint_db :
+sig
+type t
+val empty : ?name:hint_db_name -> transparent_state -> bool -> t
+val find : global_reference -> t -> search_entry
+val map_none : t -> full_hint list
+val map_all : global_reference -> t -> full_hint list
+val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list
+val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list
+val map_auto : (global_reference * 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 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 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) ->
+ t -> 'a -> 'a
+
+end =
+struct
type t = {
hintdb_state : Names.transparent_state;
@@ -421,20 +450,22 @@ module Hint_db = 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 : (global_reference option * stored_data) list;
+ hintdb_name : string option;
}
let next_hint_id db =
let h = db.hintdb_max_id in
{ db with hintdb_max_id = succ db.hintdb_max_id }, h
- let empty st use_dn = { hintdb_state = st;
+ let empty ?name st use_dn = { hintdb_state = st;
hintdb_cut = PathEmpty;
hintdb_unfolds = (Id.Set.empty, Cset.empty);
hintdb_max_id = 0;
use_dn = use_dn;
hintdb_map = Constr_map.empty;
- hintdb_nopat = [] }
+ hintdb_nopat = [];
+ hintdb_name = name; }
let find key db =
try Constr_map.find key db.hintdb_map
@@ -502,7 +533,7 @@ module Hint_db = struct
| _ -> false
let addkv gr id v db =
- let idv = id, v in
+ let idv = id, { v with db = db.hintdb_name } in
let k = match gr with
| Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr &&
is_unfold v.code.obj then None else Some gr
@@ -606,8 +637,6 @@ type hint_db = Hint_db.t
type hint_db_table = hint_db Hintdbmap.t ref
-type hint_db_name = string
-
(** Initially created hint databases, for typeclasses and rewrite *)
let typeclasses_db = "typeclass_instances"
@@ -684,6 +713,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
poly = poly;
pat = Some pat;
name = name;
+ db = None;
code = with_uid (Give_exact (c, cty, ctx)); })
let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
@@ -704,6 +734,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
poly = poly;
pat = Some pat;
name = name;
+ db = None;
code = with_uid (Res_pf(c,cty,ctx)); })
else begin
if not eapply then failwith "make_apply_entry";
@@ -715,6 +746,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
poly = poly;
pat = Some pat;
name = name;
+ db = None;
code = with_uid (ERes_pf(c,cty,ctx)); })
end
| _ -> failwith "make_apply_entry"
@@ -799,6 +831,7 @@ let make_unfold eref =
poly = false;
pat = None;
name = PathHints [g];
+ db = None;
code = with_uid (Unfold_nth eref) })
let make_extern pri pat tacast =
@@ -809,6 +842,7 @@ let make_extern pri pat tacast =
poly = false;
pat = pat;
name = PathAny;
+ db = None;
code = with_uid (Extern tacast) })
let make_mode ref m =
@@ -832,6 +866,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
poly = poly;
pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
name = name;
+ db = None;
code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
@@ -845,7 +880,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
let get_db dbname =
try searchtable_map dbname
- with Not_found -> Hint_db.empty empty_transparent_state false
+ with Not_found -> Hint_db.empty ~name:dbname empty_transparent_state false
let add_hint dbname hintlist =
let check (_, h) =
@@ -905,7 +940,7 @@ type hint_obj = {
let load_autohint _ (kn, h) =
let name = h.hint_name in
match h.hint_action with
- | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
+ | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b)
| AddTransparency (grs, b) -> add_transparency name grs b
| AddHints hints -> add_hint name hints
| RemoveHints grs -> remove_hint name grs
@@ -1262,11 +1297,11 @@ let make_db_list dbnames =
let pr_hint_elt (c, _, _) = pr_constr c
let pr_hint h = match h.obj with
- | Res_pf (c, _) -> (str"apply " ++ pr_hint_elt c)
- | ERes_pf (c, _) -> (str"eapply " ++ pr_hint_elt c)
+ | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
+ | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c)
| Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c)
| Res_pf_THEN_trivial_fail (c, _) ->
- (str"apply " ++ pr_hint_elt c ++ str" ; trivial")
+ (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial")
| Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c)
| Extern tac ->
let env =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 6f5ee8ba5e..411540aa1b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -43,11 +43,14 @@ type hints_path_atom =
(* For forward hints, their names is the list of projections *)
| PathAny
+type hint_db_name = string
+
type 'a with_metadata = private {
pri : int; (** A number between 0 and 4, 4 = lower priority *)
poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *)
pat : constr_pattern option; (** A pattern for the concl of the Goal *)
name : hints_path_atom; (** A potential name to refer to the hint *)
+ db : hint_db_name option;
code : 'a; (** the tactic to apply when the concl matches pat *)
}
@@ -77,7 +80,7 @@ val pp_hint_mode : hint_mode -> Pp.std_ppcmds
module Hint_db :
sig
type t
- val empty : transparent_state -> bool -> t
+ val empty : ?name:hint_db_name -> transparent_state -> bool -> t
val find : global_reference -> t -> search_entry
val map_none : t -> full_hint list
@@ -113,8 +116,6 @@ module Hint_db :
val unfolds : t -> Id.Set.t * Cset.t
end
-type hint_db_name = string
-
type hint_db = Hint_db.t
type hnf = bool
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 642bf520b1..40b600c890 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -202,11 +202,11 @@ let inversion_scheme env sigma t sort dep_option inv_op =
tclTHEN intro (onLastHypId inv_op)) pf)
in
let pfterm = List.hd (Proof.partial_proof pf) in
- let global_named_context = Global.named_context () in
+ let global_named_context = Global.named_context_val () in
let ownSign = ref begin
fold_named_context
(fun env d sign ->
- if mem_named_context (get_id d) global_named_context then sign
+ if mem_named_context_val (get_id d) global_named_context then sign
else Context.Named.add d sign)
invEnv ~init:Context.Named.empty
end in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 87fdcf14d4..66da9ee182 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -322,7 +322,7 @@ module New = struct
try
Refiner.catch_failerror e;
tclUNIT ()
- with e -> tclZERO e
+ with e when CErrors.noncritical e -> tclZERO e
(* spiwack: I chose to give the Ltac + the same semantics as
[Proofview.tclOR], however, for consistency with the or-else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2d901c2dbc..d2e5d8525d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -48,7 +48,11 @@ let inj_with_occurrences e = (AllOccurrences,e)
let dloc = Loc.ghost
-let typ_of env sigma c = Retyping.get_type_of env (Sigma.to_evar_map sigma) c
+let typ_of env sigma c =
+ let open Retyping in
+ try get_type_of ~lax:true env (Sigma.to_evar_map sigma) c
+ with RetypeError e ->
+ user_err_loc (Loc.ghost, "", print_retype_error e)
open Goptions
@@ -179,10 +183,10 @@ let introduction ?(check=true) id =
let gl = Proofview.Goal.assume gl in
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
- let hyps = Proofview.Goal.hyps gl in
+ let hyps = named_context_val (Proofview.Goal.env gl) in
let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
- let () = if check && mem_named_context id hyps then
+ let () = if check && mem_named_context_val id hyps then
errorlabstrm "Tactics.introduction"
(str "Variable " ++ pr_id id ++ str " is already declared.")
in
@@ -518,7 +522,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
let (sp', u') = check_mutind env sigma n ar in
if not (eq_mind sp sp') then
error "Fixpoints should be on the same mutual inductive declaration.";
- if mem_named_context f (named_context_of_val sign) then
+ if mem_named_context_val f sign then
errorlabstrm "Logic.prim_refiner"
(str "Name " ++ pr_id f ++ str " already used in the environment");
mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
@@ -571,7 +575,7 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
| [] -> sign
| (f, ar) :: oth ->
let open Context.Named.Declaration in
- if mem_named_context f (named_context_of_val sign) then
+ if mem_named_context_val f sign then
error "Name already used in the environment.";
mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
in
@@ -1937,9 +1941,7 @@ let exact_check c =
let cast_no_check cast c =
Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
- Refine.refine ~unsafe:true { run = begin fun sigma ->
- Sigma.here (Term.mkCast (c, cast, concl)) sigma
- end }
+ exact_no_check (Term.mkCast (c, cast, concl))
end }
let vm_cast_no_check c = cast_no_check Term.VMcast c
@@ -1976,7 +1978,7 @@ let assumption =
in
if is_same_type then
(Proofview.Unsafe.tclEVARS sigma) <*>
- Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
+ exact_no_check (mkVar (get_id decl))
else arec gl only_eq rest
in
let assumption_tac = { enter = begin fun gl ->
@@ -2793,7 +2795,7 @@ let old_generalize_dep ?(with_let=false) c gl =
let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
let tothin' =
match kind_of_term c with
- | Var id when mem_named_context id sign && not (Id.List.mem id init_ids)
+ | Var id when mem_named_context_val id (val_of_named_context sign) && not (Id.List.mem id init_ids)
-> id::tothin
| _ -> tothin
in
@@ -2807,6 +2809,8 @@ let old_generalize_dep ?(with_let=false) c gl =
in
let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
(cl',project gl) in
+ (** Check that the generalization is indeed well-typed *)
+ let (evd, _) = Typing.type_of env evd cl'' in
let args = Context.Named.to_instance to_quantify_rev in
tclTHENLIST
[tclEVARS evd;
@@ -2819,10 +2823,12 @@ let generalize_dep ?(with_let = false) c =
(** *)
let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ let env = Proofview.Goal.env gl in
let newcl, evd =
List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr
(Tacmach.New.pf_concl gl,Tacmach.New.project gl)
in
+ let (evd, _) = Typing.type_of env evd newcl in
let map ((_, c, b),_) = if Option.is_empty b then Some c else None in
let tac = apply_type newcl (List.map_filter map lconstr) in
Sigma.Unsafe.of_pair (tac, evd)
@@ -2943,8 +2949,8 @@ let unfold_body x =
let open Context.Named.Declaration in
Proofview.Goal.enter { enter = begin fun gl ->
(** We normalize the given hypothesis immediately. *)
- let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
- let xval = match Context.Named.lookup x hyps with
+ let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
+ let xval = match Environ.lookup_named x env with
| LocalAssum _ -> errorlabstrm "unfold_body"
(pr_id x ++ str" is not a defined hypothesis.")
| LocalDef (_,xval,_) -> xval
@@ -4366,7 +4372,7 @@ let induction_gen clear_flag isrec with_evars elim
let cls = Option.default allHypsAndConcl cls in
let t = typ_of env sigma c in
let is_arg_pure_hyp =
- isVar c && not (mem_named_context (destVar c) (Global.named_context()))
+ isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ()))
&& lbind == NoBindings && not with_evars && Option.is_empty eqname
&& clear_flag == None
&& has_generic_occurrences_but_goal cls (destVar c) env ccl in
@@ -4413,7 +4419,7 @@ let induction_gen_l isrec with_evars elim names lc =
| [] -> Proofview.tclUNIT ()
| c::l' ->
match kind_of_term c with
- | Var id when not (mem_named_context id (Global.named_context()))
+ | Var id when not (mem_named_context_val id (Global.named_context_val ()))
&& not with_evars ->
let _ = newlc:= id::!newlc in
atomize_list l'
@@ -4835,7 +4841,7 @@ let abstract_subproof id gk tac =
let open Context.Named.Declaration in
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
- let current_sign = Global.named_context()
+ let current_sign = Global.named_context_val ()
and global_sign = Proofview.Goal.hyps gl in
let sigma = Sigma.to_evar_map sigma in
let evdref = ref sigma in
@@ -4843,8 +4849,8 @@ let abstract_subproof id gk tac =
List.fold_right
(fun d (s1,s2) ->
let id = get_id d in
- if mem_named_context id current_sign &&
- interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d
+ if mem_named_context_val id current_sign &&
+ interpretable_as_section_decl evdref (lookup_named_val id current_sign) d
then (s1,push_named_context_val d s2)
else (Context.Named.add d s1,s2))
global_sign (Context.Named.empty, empty_named_context_val) in
@@ -4969,7 +4975,7 @@ module New = struct
let reduce_after_refine =
reduce
(Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]})
- {onhyps=Some []; concl_occs=AllOccurrences }
+ {onhyps=None; concl_occs=AllOccurrences }
let refine ?unsafe c =
Refine.refine ?unsafe c <*>
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 07:45:42 +0000