aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml82
-rw-r--r--tactics/auto.mli10
-rw-r--r--tactics/class_tactics.ml411
-rw-r--r--tactics/class_tactics.mli10
-rw-r--r--tactics/eauto.ml45
-rw-r--r--tactics/equality.ml31
-rw-r--r--tactics/hints.ml306
-rw-r--r--tactics/hints.mli92
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tactics.ml57
11 files changed, 666 insertions, 384 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 962af4b5c5..bc6448577f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -35,6 +35,10 @@ open Hints
let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
+let compute_secvars gl =
+ let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+ secvars_of_hyps hyps
+
(* tell auto not to reuse already instantiated metas in unification (for
compatibility, since otherwise, apply succeeds oftener) *)
@@ -260,31 +264,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
(**************************************************************************)
@@ -301,12 +299,13 @@ let flags_of_state st =
let auto_flags_of_state st =
auto_unif_flags_of full_transparent_state st false
-let hintmap_of hdc concl =
+let hintmap_of secvars hdc concl =
match hdc with
- | None -> Hint_db.map_none
+ | None -> Hint_db.map_none ~secvars
| Some hdc ->
- if occur_existential concl then Hint_db.map_existential hdc concl
- else Hint_db.map_auto hdc concl
+ if occur_existential concl then
+ Hint_db.map_existential ~secvars hdc concl
+ else Hint_db.map_auto ~secvars hdc concl
let exists_evaluable_reference env = function
| EvalConstRef _ -> true
@@ -331,22 +330,23 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
in
Proofview.Goal.enter { enter = begin fun gl ->
let concl = Tacmach.New.pf_nf_concl gl in
+ let secvars = compute_secvars gl in
Tacticals.New.tclFIRST
((dbg_assumption dbg)::intro_tac::
(List.map Tacticals.New.tclCOMPLETE
- (trivial_resolve dbg mod_delta db_list local_db concl)))
+ (trivial_resolve dbg mod_delta db_list local_db secvars concl)))
end }
-and my_find_search_nodelta db_list local_db hdc concl =
+and my_find_search_nodelta db_list local_db secvars hdc concl =
List.map (fun hint -> (None,hint))
- (List.map_append (hintmap_of hdc concl) (local_db::db_list))
+ (List.map_append (hintmap_of secvars hdc concl) (local_db::db_list))
and my_find_search mod_delta =
if mod_delta then my_find_search_delta
else my_find_search_nodelta
-and my_find_search_delta db_list local_db hdc concl =
- let f = hintmap_of hdc concl in
+and my_find_search_delta db_list local_db secvars hdc concl =
+ let f = hintmap_of secvars hdc concl in
if occur_existential concl then
List.map_append
(fun db ->
@@ -366,16 +366,16 @@ and my_find_search_delta db_list local_db hdc concl =
let (ids, csts as st) = Hint_db.transparent_state db in
let flags, l =
let l =
- match hdc with None -> Hint_db.map_none db
+ match hdc with None -> Hint_db.map_none ~secvars db
| Some hdc ->
if (Id.Pred.is_empty ids && Cpred.is_empty csts)
- then Hint_db.map_auto hdc concl db
- else Hint_db.map_existential hdc concl db
+ then Hint_db.map_auto ~secvars hdc concl db
+ else Hint_db.map_existential ~secvars hdc concl db
in auto_flags_of_state st, l
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,9 +394,16 @@ 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 =
+and trivial_resolve dbg mod_delta db_list local_db secvars cl =
try
let head =
try let hdconstr = decompose_app_bound cl in
@@ -405,7 +412,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
in
List.map (tac_of_hint dbg db_list local_db cl)
(priority
- (my_find_search mod_delta db_list local_db head cl))
+ (my_find_search mod_delta db_list local_db secvars head cl))
with Not_found -> []
(** The use of the "core" database can be de-activated by passing
@@ -443,7 +450,7 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
(* The classical Auto tactic *)
(**************************************************************************)
-let possible_resolve dbg mod_delta db_list local_db cl =
+let possible_resolve dbg mod_delta db_list local_db secvars cl =
try
let head =
try let hdconstr = decompose_app_bound cl in
@@ -451,7 +458,7 @@ let possible_resolve dbg mod_delta db_list local_db cl =
with Bound -> None
in
List.map (tac_of_hint dbg db_list local_db cl)
- (my_find_search mod_delta db_list local_db head cl)
+ (my_find_search mod_delta db_list local_db secvars head cl)
with Not_found -> []
let extend_local_db decl db gl =
@@ -482,11 +489,12 @@ let search d n mod_delta db_list local_db =
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
( Proofview.Goal.enter { enter = begin fun gl ->
let concl = Tacmach.New.pf_nf_concl gl in
+ let secvars = compute_secvars gl in
let d' = incr_dbg d in
Tacticals.New.tclFIRST
(List.map
(fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
- (possible_resolve d mod_delta db_list local_db concl))
+ (possible_resolve d mod_delta db_list local_db secvars concl))
end }))
end []
in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 1608a0ea63..3befaaadeb 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -15,7 +15,7 @@ open Pattern
open Decl_kinds
open Hints
-val priority : ('a * full_hint) list -> ('a * full_hint) list
+val compute_secvars : ('a,'b) Proofview.Goal.t -> Id.Pred.t
val default_search_depth : int ref
@@ -50,17 +50,15 @@ val new_auto : ?debug:Tacexpr.debug ->
(** auto with default search depth and with the hint database "core" *)
val default_auto : unit Proofview.tactic
-(** auto with all hint databases except the "v62" compatibility database *)
+(** auto with all hint databases *)
val full_auto : ?debug:Tacexpr.debug ->
int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic
-(** auto with all hint databases except the "v62" compatibility database
- and doing delta *)
+(** auto with all hint databases and doing delta *)
val new_full_auto : ?debug:Tacexpr.debug ->
int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic
-(** auto with default search depth and with all hint databases
- except the "v62" compatibility database *)
+(** auto with default search depth and with all hint databases *)
val default_full_auto : unit Proofview.tactic
(** The generic form of auto (second arg [None] means all bases) *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c5b0e149a8..d1ae85e7be 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -9,7 +9,6 @@
(* TODO:
- Find an interface allowing eauto to backtrack when shelved goals remain,
e.g. to force instantiations.
- - unique solutions
*)
open Pp
@@ -43,7 +42,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 +58,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
@@ -98,7 +92,7 @@ open Goptions
let _ =
declare_bool_option
{ optsync = true;
- optdepr = false;
+ optdepr = true;
optname = "do typeclass search modulo eta conversion";
optkey = ["Typeclasses";"Modulo";"Eta"];
optread = get_typeclasses_modulo_eta;
@@ -133,22 +127,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
@@ -186,6 +180,12 @@ let set_typeclasses_depth =
optread = get_typeclasses_depth;
optwrite = set_typeclasses_depth; }
+type search_strategy = Dfs | Bfs
+
+let set_typeclasses_strategy = function
+ | Dfs -> set_typeclasses_iterative_deepening false
+ | Bfs -> set_typeclasses_iterative_deepening true
+
let pr_ev evs ev =
Printer.pr_constr_env (Goal.V82.env evs ev) evs
(Evarutil.nf_evar evs (Goal.V82.concl evs ev))
@@ -245,12 +245,11 @@ let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
end }
(** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine poly flags =
+let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
let open Clenv in
- { enter = begin fun gls ((c, t, ctx),n,clenv) ->
- let env = Proofview.Goal.env gls in
- let concl = Proofview.Goal.concl gls in
- Refine.refine ~unsafe:true { Sigma.run = fun sigma ->
+ let env = Proofview.Goal.env gls in
+ let concl = Proofview.Goal.concl gls in
+ Refine.refine ~unsafe:true { Sigma.run = fun sigma ->
let sigma = Sigma.to_evar_map sigma in
let sigma, term, ty =
if poly then
@@ -265,15 +264,20 @@ let unify_resolve_refine poly flags =
let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
let term = applistc term (List.map (fun x -> x.hole_evar) cl.cl_holes) in
let sigma' =
- let evdref = ref sigma' in
- if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta
- evdref cl.cl_concl concl) then
- Type_errors.error_actual_type env
- {Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
- concl;
- !evdref
+ Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta
+ cl.cl_concl concl sigma'
in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') }
- end }
+
+let unify_resolve_refine poly flags gl clenv =
+ Proofview.tclORELSE
+ (unify_resolve_refine poly flags gl clenv)
+ (fun ie ->
+ match fst ie with
+ | Evarconv.UnableToUnify _ ->
+ Tacticals.New.tclZEROMSG (str "Unable to unify")
+ | e when CErrors.noncritical e ->
+ Tacticals.New.tclZEROMSG (str "Unexpected error")
+ | _ -> iraise ie)
(** Dealing with goals of the form A -> B and hints of the form
C -> A -> B.
@@ -285,18 +289,20 @@ let clenv_of_prods poly nprods (c, clenv) gl =
let ty = Retyping.get_type_of (Proofview.Goal.env gl)
(Sigma.to_evar_map (Proofview.Goal.sigma gl)) c in
let diff = nb_prod ty - nprods in
- if Pervasives.(>=) diff 0 then
- (* Was Some clenv... *)
- Some (Some diff,
- Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
- else None
+ if Pervasives.(>=) diff 0 then
+ (* Was Some clenv... *)
+ Some (Some diff,
+ Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
+ else None
let with_prods nprods poly (c, clenv) f =
if get_typeclasses_limit_intros () then
Proofview.Goal.nf_enter { enter = begin fun gl ->
- match clenv_of_prods poly nprods (c, clenv) gl with
- | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
- | Some (diff, clenv') -> f.enter gl (c, diff, clenv') end }
+ try match clenv_of_prods poly nprods (c, clenv) gl with
+ | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+ | Some (diff, clenv') -> f.enter gl (c, diff, clenv')
+ with e when CErrors.noncritical e ->
+ Tacticals.New.tclZEROMSG (CErrors.print e) end }
else Proofview.Goal.nf_enter
{ enter = begin fun gl ->
if Int.equal nprods 0 then f.enter gl (c, None, clenv)
@@ -311,7 +317,7 @@ let matches_pattern concl pat =
if Constr_matching.is_matching env sigma pat concl then
Proofview.tclUNIT ()
else
- Tacticals.New.tclZEROMSG (str "conclPattern")
+ Tacticals.New.tclZEROMSG (str "pattern does not match")
in
Proofview.Goal.enter { enter = fun gl ->
let env = Proofview.Goal.env gl in
@@ -339,12 +345,21 @@ let pr_gls sigma gls =
let shelve_dependencies gls =
let open Proofview in
tclEVARMAP >>= fun sigma ->
- (if !typeclasses_debug > 1 then
- Feedback.msg_debug (str" shelving goals: " ++ pr_gls sigma gls);
+ (if !typeclasses_debug > 1 && List.length gls > 0 then
+ Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls);
shelve_goals gls)
+let hintmap_of hdc secvars concl =
+ match hdc with
+ | None -> fun db -> Hint_db.map_none secvars db
+ | Some hdc ->
+ fun db ->
+ if Hint_db.use_dn db then (* Using dnet *)
+ Hint_db.map_eauto secvars hdc concl db
+ else Hint_db.map_existential secvars hdc concl db
+
(** Hack to properly solve dependent evars that are typeclasses *)
-let rec e_trivial_fail_db only_classes db_list local_db =
+let rec e_trivial_fail_db only_classes db_list local_db secvars =
let open Tacticals.New in
let open Tacmach.New in
let trivial_fail =
@@ -355,13 +370,13 @@ let rec e_trivial_fail_db only_classes db_list local_db =
let d = pf_last_hyp gl in
let hintl = make_resolve_hyp env sigma d in
let hints = Hint_db.add_list env sigma hintl local_db in
- e_trivial_fail_db only_classes db_list hints
+ e_trivial_fail_db only_classes db_list hints secvars
end }
in
let trivial_resolve =
Proofview.Goal.nf_enter { enter =
begin fun gl ->
- let tacs = e_trivial_resolve db_list local_db only_classes
+ let tacs = e_trivial_resolve db_list local_db secvars only_classes
(project gl) (pf_concl gl) in
tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs)
end}
@@ -372,69 +387,77 @@ let rec e_trivial_fail_db only_classes db_list local_db =
in
tclFIRST (List.map tclCOMPLETE tacl)
-and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
+and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl =
let open Proofview.Notations in
let prods, concl = decompose_prod_assum concl in
let nprods = List.length prods in
let freeze =
try
- let cl = Typeclasses.class_info (fst hdc) in
- if cl.cl_strict then
- Evd.evars_of_term concl
- else Evar.Set.empty
+ match hdc with
+ | Some (hd,_) when only_classes ->
+ let cl = Typeclasses.class_info hd in
+ if cl.cl_strict then
+ Evd.evars_of_term concl
+ else Evar.Set.empty
+ | _ -> Evar.Set.empty
with e when CErrors.noncritical e -> Evar.Set.empty
in
+ let hint_of_db = hintmap_of hdc secvars concl in
let hintl =
List.map_append
(fun db ->
- let tacs =
- if Hint_db.use_dn db then (* Using dnet *)
- Hint_db.map_eauto hdc concl db
- else Hint_db.map_existential hdc concl db
- in
+ let tacs = hint_of_db db in
let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
List.map (fun x -> (flags, x)) tacs)
(local_db::db_list)
in
let tac_of_hint =
- fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
+ fun (flags, {pri = b; pat = p; poly = poly; code = t; secvars; 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 ->
- (matches_pattern concl p) <*>
- ((unify_resolve_refine poly flags).enter gl clenv)})
+ matches_pattern concl p <*>
+ unify_resolve_refine poly flags gl clenv})
in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
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) <*>
- ((unify_resolve_refine poly flags).enter gl clenv)})) in
+ matches_pattern concl p <*>
+ unify_resolve_refine poly flags gl clenv})) in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
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)
(fun (gls, ()) -> shelve_dependencies gls)
- | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
+ | Give_exact (c,clenv) ->
+ if get_typeclasses_filtered_unification () then
+ let tac =
+ matches_pattern concl p <*>
+ Proofview.Goal.nf_enter
+ { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
+ Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
+ else
+ Proofview.V82.tactic (e_give_exact flags poly (c,clenv))
| Res_pf_THEN_trivial_fail (term,cl) ->
let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
let snd = if complete then Tacticals.New.tclIDTAC
- else e_trivial_fail_db only_classes db_list local_db in
+ else e_trivial_fail_db only_classes db_list local_db secvars in
Tacticals.New.tclTHEN fst snd
| Unfold_nth c ->
let tac = Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]) in
@@ -445,7 +468,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
@@ -454,17 +477,17 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
| _ -> (tac, b, false, name, lazy (pr_hint t ++ pp))
in List.map tac_of_hint hintl
-and e_trivial_resolve db_list local_db only_classes sigma concl =
+and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
+ let hd = try Some (decompose_app_bound concl) with Bound -> None in
try
- e_my_find_search db_list local_db
- (decompose_app_bound concl) true only_classes sigma concl
- with Bound | Not_found -> []
+ e_my_find_search db_list local_db secvars hd true only_classes sigma concl
+ with Not_found -> []
-let e_possible_resolve db_list local_db only_classes sigma concl =
+let e_possible_resolve db_list local_db secvars only_classes sigma concl =
+ let hd = try Some (decompose_app_bound concl) with Bound -> None in
try
- e_my_find_search db_list local_db
- (decompose_app_bound concl) false only_classes sigma concl
- with Bound | Not_found -> []
+ e_my_find_search db_list local_db secvars hd false only_classes sigma concl
+ with Not_found -> []
let cut_of_hints h =
List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
@@ -544,10 +567,16 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
let name = PathHints [VarRef id] in
let hints =
if is_class then
- let hints = build_subclasses ~check:false env sigma (VarRef id) None in
+ let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in
(List.map_append
- (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
- (true,false,Flags.is_verbose()) pri false
+ (fun (path,info,c) ->
+ let info =
+ { info with Vernacexpr.hint_pattern =
+ Option.map (Constrintern.intern_constr_pattern env)
+ info.Vernacexpr.hint_pattern }
+ in
+ make_resolves env sigma ~name:(PathHints path)
+ (true,false,Flags.is_verbose()) info false
(IsConstr (c,Univ.ContextSet.empty)))
hints)
else []
@@ -572,7 +601,7 @@ let make_hints g st only_classes sign =
in
if consider then
let hint =
- pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
+ pf_apply make_resolve_hyp g st (true,false,false) only_classes empty_hint_info hyp
in hint @ hints
else hints)
([]) sign
@@ -641,7 +670,7 @@ module V85 = struct
let env = Goal.V82.env s g' in
let context = Environ.named_context_of_val (Goal.V82.hyps s g') in
let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
- (true,false,false) info.only_classes None (List.hd context) in
+ (true,false,false) info.only_classes empty_hint_info (List.hd context) in
let ldb = Hint_db.add_list env s hint info.hints in
(g', { info with is_evar = None; hints = ldb;
auto_last_tac = lazy (str"intro") })) gls
@@ -678,7 +707,8 @@ module V85 = struct
let env = Goal.V82.env s gl in
let concl = Goal.V82.concl s gl in
let tacgl = {it = gl; sigma = s;} in
- let poss = e_possible_resolve hints info.hints info.only_classes s concl in
+ let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in
+ let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in
let unique = is_unique env concl in
let rec aux i foundone = function
| (tac, _, extern, name, pp) :: tl ->
@@ -884,19 +914,20 @@ module V85 = struct
let eauto_tac hints =
then_tac normevars_tac (or_tac (hints_tac hints) intro_tac)
- let eauto_tac depth hints =
- if get_typeclasses_iterative_deepening () then
- match depth with
- | None -> fix_iterative (eauto_tac hints)
- | Some depth -> fix_iterative_limit depth (eauto_tac hints)
- else
- match depth with
- | None -> fix (eauto_tac hints)
- | Some depth -> fix_limit depth (eauto_tac hints)
-
- let real_eauto ?depth unique st hints p evd =
+ let eauto_tac strategy depth hints =
+ match strategy with
+ | Bfs ->
+ begin match depth with
+ | None -> fix_iterative (eauto_tac hints)
+ | Some depth -> fix_iterative_limit depth (eauto_tac hints) end
+ | Dfs ->
+ match depth with
+ | None -> fix (eauto_tac hints)
+ | Some depth -> fix_limit depth (eauto_tac hints)
+
+ let real_eauto ?depth strategy unique st hints p evd =
let res =
- run_on_evars ~st ~unique p evd hints (eauto_tac depth hints)
+ run_on_evars ~st ~unique p evd hints (eauto_tac strategy depth hints)
in
match res with
| None -> evd
@@ -909,12 +940,18 @@ module V85 = struct
let resolve_all_evars_once debug depth unique p evd =
let db = searchtable_map typeclasses_db in
- real_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd
-
- let eauto85 ?(only_classes=true) ?st depth hints g =
+ let strategy = if get_typeclasses_iterative_deepening () then Bfs else Dfs in
+ real_eauto ?depth strategy unique (Hint_db.transparent_state db) [db] p evd
+
+ let eauto85 ?(only_classes=true) ?st ?strategy depth hints g =
+ let strategy =
+ match strategy with
+ | None -> if get_typeclasses_iterative_deepening () then Bfs else Dfs
+ | Some s -> s
+ in
let gl = { it = make_autogoal ~only_classes ?st
(cut_of_hints hints) None g; sigma = project g; } in
- match run_tac (eauto_tac depth hints) gl with
+ match run_tac (eauto_tac strategy depth hints) gl with
| None -> raise Not_found
| Some {it = goals; sigma = s; } ->
{it = List.map fst goals; sigma = s;}
@@ -990,6 +1027,18 @@ module Search = struct
Evd.add sigma gl evi')
sigma goals
+ let fail_if_nonclass info =
+ Proofview.Goal.enter { enter = fun gl ->
+ let gl = Proofview.Goal.assume gl in
+ let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+ if is_class_type sigma (Proofview.Goal.concl gl) then
+ Proofview.tclUNIT ()
+ else (if !typeclasses_debug > 1 then
+ Feedback.msg_debug (pr_depth info.search_depth ++
+ str": failure due to non-class subgoal " ++
+ pr_ev sigma (Proofview.Goal.goal gl));
+ Proofview.tclZERO NotApplicableEx) }
+
(** The general hint application tactic.
tac1 + tac2 .... The choice of OR or ORELSE is determined
depending on the dependencies of the goal and the unique/Prop
@@ -1009,8 +1058,9 @@ module Search = struct
Printer.pr_constr_env (Goal.env gl) s concl ++
(if backtrack then str" with backtracking"
else str" without backtracking"));
+ let secvars = compute_secvars gl in
let poss =
- e_possible_resolve hints info.search_hints info.search_only_classes s concl in
+ e_possible_resolve hints info.search_hints secvars info.search_only_classes s concl in
(* If no goal depends on the solution of this one or the
instances are irrelevant/assumed to be unique, then
we don't need to backtrack, as long as no evar appears in the goal
@@ -1021,13 +1071,18 @@ module Search = struct
let foundone = ref false in
let rec onetac e (tac, pat, b, name, pp) tl =
let derivs = path_derivate info.search_cut name in
- (if !typeclasses_debug > 1 then
- Feedback.msg_debug
- (pr_depth (!idx :: info.search_depth) ++ str": trying " ++
+ let pr_error ie =
+ if !typeclasses_debug > 1 then
+ let msg =
+ pr_depth (!idx :: info.search_depth) ++ str": " ++
Lazy.force pp ++
(if !foundone != true then
str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
- else mt ())));
+ else mt ())
+ in
+ Feedback.msg_debug (msg ++ str " failed with " ++ CErrors.iprint ie)
+ else ()
+ in
let tac_of gls i j = Goal.nf_enter { enter = fun gl' ->
let sigma' = Goal.sigma gl' in
let s' = Sigma.to_evar_map sigma' in
@@ -1069,12 +1124,12 @@ module Search = struct
else tclDISPATCH
(List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j))))
in
- let finish sigma =
+ let finish nestedshelf sigma =
let filter ev =
try
let evi = Evd.find_undefined sigma ev in
if info.search_only_classes then
- Some (ev, is_class_type sigma (Evd.evar_concl evi))
+ Some (ev, not (is_class_type sigma (Evd.evar_concl evi)))
else Some (ev, true)
with Not_found -> None
in
@@ -1092,9 +1147,9 @@ module Search = struct
begin
(* Some existentials produced by the original tactic were not solved
in the subgoals, turn them into subgoals now. *)
- let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in
- let shelved = List.map fst shelved and goals = List.map fst goals in
- if !typeclasses_debug > 1 then
+ let shelved, goals = List.partition (fun (ev, s) -> s) remaining in
+ let shelved = List.map fst shelved @ nestedshelf and goals = List.map fst goals in
+ if !typeclasses_debug > 1 && not (List.is_empty shelved && List.is_empty goals) then
Feedback.msg_debug
(str"Adding shelved subgoals to the search: " ++
prlist_with_sep spc (pr_ev sigma) goals ++
@@ -1107,13 +1162,23 @@ module Search = struct
with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>=
fun s -> result s i (Some (Option.default 0 k + j)))
end
- in res <*> tclEVARMAP >>= finish
+ in with_shelf res >>= fun (sh, ()) ->
+ tclEVARMAP >>= finish sh
in
if path_matches derivs [] then aux e tl
- else ortac
- (with_shelf tac >>= fun s ->
+ else
+ let filter =
+ if false (* in 8.6, still allow non-class subgoals
+ info.search_only_classes *) then fail_if_nonclass info
+ else Proofview.tclUNIT ()
+ in
+ ortac
+ (with_shelf (tac <*> filter) >>= fun s ->
let i = !idx in incr idx; result s i None)
- (fun e' -> aux (merge_exceptions e e') tl)
+ (fun e' ->
+ if CErrors.noncritical (fst e') then
+ (pr_error e'; aux (merge_exceptions e e') tl)
+ else iraise e')
and aux e = function
| x :: xs -> onetac e x xs
| [] ->
@@ -1143,10 +1208,11 @@ module Search = struct
let decl = Tacmach.New.pf_last_hyp gl in
let hint =
make_resolve_hyp env s (Hint_db.transparent_state info.search_hints)
- (true,false,false) info.search_only_classes None decl in
+ (true,false,false) info.search_only_classes empty_hint_info decl in
let ldb = Hint_db.add_list env s hint info.search_hints in
let info' =
- { info with search_hints = ldb; last_tac = lazy (str"intro") }
+ { info with search_hints = ldb; last_tac = lazy (str"intro");
+ search_depth = 1 :: 1 :: info.search_depth }
in kont info'
let intro info kont =
@@ -1174,9 +1240,12 @@ module Search = struct
unit Proofview.tactic =
let open Proofview in
let open Proofview.Notations in
- let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
- let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
- search_tac hints depth 1 info
+ if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
+ Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
+ else
+ let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
+ let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+ search_tac hints depth 1 info
let search_tac ?(st=full_transparent_state) only_classes dep hints depth =
let open Proofview in
@@ -1207,16 +1276,24 @@ module Search = struct
| (e,ie) -> Proofview.tclZERO ~info:ie e)
in aux 1
- let eauto_tac ?(st=full_transparent_state) ~only_classes ~depth ~dep hints =
+ let eauto_tac ?(st=full_transparent_state) ?(unique=false)
+ ~only_classes ?strategy ~depth ~dep hints =
+ let open Proofview in
let tac =
let search = search_tac ~st only_classes dep hints in
- if get_typeclasses_iterative_deepening () then
+ let dfs =
+ match strategy with
+ | None -> not (get_typeclasses_iterative_deepening ())
+ | Some Dfs -> true
+ | Some Bfs -> false
+ in
+ if dfs then
+ let depth = match depth with None -> -1 | Some d -> d in
+ search depth
+ else
match depth with
| None -> fix_iterative search
| Some l -> fix_iterative_limit l search
- else
- let depth = match depth with None -> -1 | Some d -> d in
- search depth
in
let error (e, ie) =
match e with
@@ -1226,10 +1303,28 @@ module Search = struct
Tacticals.New.tclFAIL 0 (str"Proof search failed" ++
(if Option.is_empty depth then mt()
else str" without reaching its limit"))
+ | Proofview.MoreThanOneSuccess ->
+ Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++
+ str"more than one success found")
| e -> Proofview.tclZERO ~info:ie e
- in Proofview.tclOR tac error
-
- let run_on_evars ?(unique=false) p evm tac =
+ in
+ let tac = Proofview.tclOR tac error in
+ let tac =
+ if unique then
+ Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac
+ else tac
+ in
+ with_shelf numgoals >>= fun (initshelf, i) ->
+ (if !typeclasses_debug > 1 then
+ Feedback.msg_debug (str"Starting resolution with " ++ int i ++
+ str" goal(s) under focus and " ++
+ int (List.length initshelf) ++ str " shelved goal(s)" ++
+ (if only_classes then str " in only_classes mode" else str " in regular mode") ++
+ match depth with None -> str ", unbounded"
+ | Some i -> str ", with depth limit " ++ int i));
+ tac
+
+ let run_on_evars p evm tac =
match evars_to_goals p evm with
| None -> None (* This happens only because there's no evar having p *)
| Some (goals, evm') ->
@@ -1261,16 +1356,15 @@ module Search = struct
else raise Not_found
with Logic_monad.TacticFailure _ -> raise Not_found
- let eauto depth only_classes unique dep st hints p evd =
- let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep hints in
- let res = run_on_evars ~unique p evd eauto_tac in
+ let evars_eauto depth only_classes unique dep st hints p evd =
+ let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
+ let res = run_on_evars p evd eauto_tac in
match res with
| None -> evd
| Some evd' -> evd'
- (* TODO treat unique solutions *)
let typeclasses_eauto ?depth unique st hints p evd =
- eauto depth true unique false st hints p evd
+ evars_eauto depth true unique false st hints p evd
(** Typeclasses eauto is an eauto which tries to resolve only
goals of typeclass type, and assumes that the initially selected
evars in evd are independent of the rest of the evars *)
@@ -1281,11 +1375,9 @@ module Search = struct
end
(** Binding to either V85 or Search implementations. *)
-let eauto depth ~only_classes ~st ~dep dbs =
- Search.eauto_tac ~st ~only_classes ~depth ~dep dbs
let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
- ~depth dbs =
+ ?strategy ~depth dbs =
let dbs = List.map_filter
(fun db -> try Some (searchtable_map db)
with e when CErrors.noncritical e -> None)
@@ -1293,13 +1385,13 @@ 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
+ try V85.eauto85 depth ~only_classes ~st ?strategy dbs gl
with Not_found ->
Refiner.tclFAIL 0 (str"Proof search failed") gl)
- else eauto depth ~only_classes ~st ~dep:true dbs
+ else Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs
(** We compute dependencies via a union-find algorithm.
Beware of the imperative effects on the partition structure,
@@ -1419,10 +1511,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
@@ -1442,7 +1534,7 @@ let initial_select_evars filter =
let resolve_typeclass_evars debug depth unique env evd filter split fail =
let evd =
- try Evarconv.consider_remaining_unif_problems
+ try Evarconv.solve_unif_constraints_with_heuristics
~ts:(Typeclasses.classes_transparent_state ()) env evd
with e when CErrors.noncritical e -> evd
in
@@ -1467,12 +1559,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/class_tactics.mli b/tactics/class_tactics.mli
index 8db264ad95..76760db025 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -20,7 +20,11 @@ val get_typeclasses_debug : unit -> bool
val set_typeclasses_depth : int option -> unit
val get_typeclasses_depth : unit -> int option
-val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state ->
+type search_strategy = Dfs | Bfs
+
+val set_typeclasses_strategy : search_strategy -> unit
+
+val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy ->
depth:(Int.t option) ->
Hints.hint_db_name list -> unit Proofview.tactic
@@ -36,8 +40,12 @@ module Search : sig
val eauto_tac :
?st:Names.transparent_state ->
(** The transparent_state used when working with local hypotheses *)
+ ?unique:bool ->
+ (** Should we force a unique solution *)
only_classes:bool ->
(** Should non-class goals be shelved and resolved at the end *)
+ ?strategy:search_strategy ->
+ (** Is a traversing-strategy specified? *)
depth:Int.t option ->
(** Bounded or unbounded search *)
dep:bool ->
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index ba9a2d95c8..23ff582253 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -119,12 +119,13 @@ let unify_e_resolve poly flags (c,clenv) =
(Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
end }
-let hintmap_of hdc concl =
+let hintmap_of secvars hdc concl =
match hdc with
- | None -> fun db -> Hint_db.map_none db
+ | None -> fun db -> Hint_db.map_none ~secvars db
| Some hdc ->
- if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db)
- else (fun db -> Hint_db.map_auto hdc concl db)
+ if occur_existential concl then
+ (fun db -> Hint_db.map_existential ~secvars hdc concl db)
+ else (fun db -> Hint_db.map_auto ~secvars hdc concl db)
(* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
let e_exact poly flags (c,clenv) =
@@ -142,16 +143,17 @@ let rec e_trivial_fail_db db_list local_db =
e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
end } in
Proofview.Goal.enter { enter = begin fun gl ->
+ let secvars = compute_secvars gl in
let tacl =
registered_e_assumption ::
(Tacticals.New.tclTHEN Tactics.intro next) ::
- (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl)))
+ (List.map fst (e_trivial_resolve db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
in
Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
end }
-and e_my_find_search db_list local_db hdc concl =
- let hint_of_db = hintmap_of hdc concl in
+and e_my_find_search db_list local_db secvars hdc concl =
+ let hint_of_db = hintmap_of secvars hdc concl in
let hintl =
List.map_append (fun db ->
let flags = auto_flags_of_state (Hint_db.transparent_state db) in
@@ -179,14 +181,15 @@ and e_my_find_search db_list local_db hdc concl =
in
List.map tac_of_hint hintl
-and e_trivial_resolve db_list local_db gl =
+and e_trivial_resolve db_list local_db secvars gl =
let hd = try Some (decompose_app_bound gl) with Bound -> None in
- try priority (e_my_find_search db_list local_db hd gl)
+ try priority (e_my_find_search db_list local_db secvars hd gl)
with Not_found -> []
-let e_possible_resolve db_list local_db gl =
+let e_possible_resolve db_list local_db secvars gl =
let hd = try Some (decompose_app_bound gl) with Bound -> None in
- try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl)
+ try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
+ (e_my_find_search db_list local_db secvars hd gl)
with Not_found -> []
let find_first_goal gls =
@@ -255,9 +258,11 @@ module SearchProblem = struct
let nbgl = List.length (sig_it lg) in
assert (nbgl > 0);
let g = find_first_goal lg in
+ let hyps = pf_ids_of_hyps g in
+ let secvars = secvars_of_hyps (pf_hyps g) in
let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
let assumption_tacs =
- let tacs = List.map map_assum (pf_ids_of_hyps g) in
+ let tacs = List.map map_assum hyps in
let l = filter_tactics s.tacres tacs in
List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
last_tactic = pp; dblist = s.dblist;
@@ -282,7 +287,9 @@ 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) secvars concl)
in
List.map
(fun (lgls, cost, pp) ->
@@ -345,13 +352,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 +369,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)
@@ -409,9 +416,7 @@ let eauto ?(debug=Off) np lems dbnames =
tclTRY (e_search_auto debug np lems db_list)
let full_eauto ?(debug=Off) n lems gl =
- let dbnames = current_db_names () in
- let dbnames = String.Set.remove "v62" dbnames in
- let db_list = List.map searchtable_map (String.Set.elements dbnames) in
+ let db_list = current_pure_db () in
tclTRY (e_search_auto debug n lems db_list) gl
let gen_eauto ?(debug=Off) np lems = function
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3e5b7b65ff..bb3cbad92b 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)
@@ -1163,7 +1163,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let dflt_typ = unsafe_type_of env sigma dflt in
try
let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
- let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
+ let () =
+ evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
dflt
with Evarconv.UnableToUnify _ ->
error "Cannot solve a unification problem."
@@ -1389,7 +1390,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 +1765,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..9a96b73898 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -66,6 +66,28 @@ let decompose_app_bound t =
| Proj (p, c) -> ConstRef (Projection.constant p), Array.cons c args
| _ -> raise Bound
+(** Compute the set of section variables that remain in the named context.
+ Starts from the top to the bottom of the context, stops at the first
+ different declaration between the named hyps and the section context. *)
+let secvars_of_hyps hyps =
+ let secctx = Global.named_context () in
+ let pred, all =
+ List.fold_left (fun (pred,all) decl ->
+ try let _ = Context.Named.lookup (get_id decl) hyps in
+ (* Approximation, it might be an hypothesis reintroduced with same name and unconvertible types,
+ we must allow it currently, as comparing the declarations for syntactic equality is too
+ strong a check (e.g. an unfold in a section variable would make it unusable). *)
+ (Id.Pred.add (get_id decl) pred, all)
+ with Not_found -> (pred, false))
+ (Id.Pred.empty,true) secctx
+ in
+ if all then Id.Pred.full (* If the whole section context is available *)
+ else pred
+
+let empty_hint_info =
+ let open Vernacexpr in
+ { hint_priority = None; hint_pattern = None }
+
(************************************************************************)
(* The Type of Constructions Autotactic Hints *)
(************************************************************************)
@@ -78,18 +100,25 @@ type 'a hint_ast =
| Unfold_nth of evaluable_global_reference (* Hint Unfold *)
| Extern of Genarg.glob_generic_argument (* Hint Extern *)
-type hints_path_atom =
- | PathHints of global_reference list
+
+type 'a hints_path_atom_gen =
+ | PathHints of 'a list
+ (* For forward hints, their names is the list of projections *)
| PathAny
-type hints_path =
- | PathAtom of hints_path_atom
- | PathStar of hints_path
- | PathSeq of hints_path * hints_path
- | PathOr of hints_path * hints_path
+type hints_path_atom = global_reference hints_path_atom_gen
+
+type 'a hints_path_gen =
+ | PathAtom of 'a hints_path_atom_gen
+ | PathStar of 'a hints_path_gen
+ | PathSeq of 'a hints_path_gen * 'a hints_path_gen
+ | PathOr of 'a hints_path_gen * 'a hints_path_gen
| PathEmpty
| PathEpsilon
+type pre_hints_path = Libnames.reference hints_path_gen
+type hints_path = global_reference hints_path_gen
+
type hint_term =
| IsGlobRef of global_reference
| IsConstr of constr * Univ.universe_context_set
@@ -104,11 +133,13 @@ type raw_hint = constr * types * Univ.universe_context_set
type hint = (raw_hint * clausenv) hint_ast with_uid
type 'a with_metadata = {
- pri : int; (* A number lower is higher 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 *)
- code : 'a; (* the tactic to apply when the concl matches pat *)
+ pri : int; (* A number lower is higher 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 : string option; (** The database from which the hint comes *)
+ secvars : Id.Pred.t; (* The set of section variables the hint depends on *)
+ code : 'a; (* the tactic to apply when the concl matches pat *)
}
type full_hint = hint with_metadata
@@ -369,21 +400,40 @@ let rec normalize_path h =
let path_derivate hp hint = normalize_path (path_derivate hp hint)
-let pp_hints_path_atom a =
+let pp_hints_path_atom prg a =
match a with
| PathAny -> str"_"
- | PathHints grs -> pr_sequence pr_global grs
-
-let rec pp_hints_path = function
- | PathAtom pa -> pp_hints_path_atom pa
- | PathStar (PathAtom PathAny) -> str"_*"
- | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
- | PathSeq (p, p') -> pp_hints_path p ++ spc () ++ pp_hints_path p'
- | PathOr (p, p') ->
- str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ cut () ++ spc () ++
- pp_hints_path p' ++ str ")"
+ | PathHints grs -> pr_sequence prg grs
+
+let pp_hints_path_gen prg =
+ let rec aux = function
+ | PathAtom pa -> pp_hints_path_atom prg pa
+ | PathStar (PathAtom PathAny) -> str"_*"
+ | PathStar p -> str "(" ++ aux p ++ str")*"
+ | PathSeq (p, p') -> aux p ++ spc () ++ aux p'
+ | PathOr (p, p') ->
+ str "(" ++ aux p ++ spc () ++ str"|" ++ cut () ++ spc () ++
+ aux p' ++ str ")"
| PathEmpty -> str"emp"
| PathEpsilon -> str"eps"
+ in aux
+
+let pp_hints_path = pp_hints_path_gen pr_global
+
+let glob_hints_path_atom p =
+ match p with
+ | PathHints g -> PathHints (List.map Nametab.global g)
+ | PathAny -> PathAny
+
+let glob_hints_path =
+ let rec aux = function
+ | PathAtom pa -> PathAtom (glob_hints_path_atom pa)
+ | PathStar p -> PathStar (aux p)
+ | PathSeq (p, p') -> PathSeq (aux p, aux p')
+ | PathOr (p, p') -> PathOr (aux p, aux p')
+ | PathEmpty -> PathEmpty
+ | PathEpsilon -> PathEpsilon
+ in aux
let subst_path_atom subst p =
match p with
@@ -410,7 +460,38 @@ 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 : secvars:Id.Pred.t -> t -> full_hint list
+val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+val map_existential : secvars:Id.Pred.t ->
+ (global_reference * constr array) -> constr -> t -> full_hint list
+val map_eauto : secvars:Id.Pred.t ->
+ (global_reference * constr array) -> constr -> t -> full_hint list
+val map_auto : secvars:Id.Pred.t ->
+ (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,26 +502,32 @@ 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
with Not_found -> empty_se
- let realize_tac (id,tac) = tac
+ let realize_tac secvars (id,tac) =
+ if Id.Pred.subset tac.secvars secvars then Some tac
+ else
+ (** Warn about no longer typable hint? *)
+ None
let match_mode m arg =
match m with
@@ -458,40 +545,40 @@ module Hint_db = struct
if List.is_empty modes then true
else List.exists (matches_mode args) modes
- let merge_entry db nopat pat =
+ let merge_entry secvars db nopat pat =
let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in
let h = List.merge pri_order_int h nopat in
let h = List.merge pri_order_int h pat in
- List.map realize_tac h
+ List.map_filter (realize_tac secvars) h
- let map_none db =
- merge_entry db [] []
+ let map_none ~secvars db =
+ merge_entry secvars db [] []
- let map_all k db =
+ let map_all ~secvars k db =
let se = find k db in
- merge_entry db se.sentry_nopat se.sentry_pat
+ merge_entry secvars db se.sentry_nopat se.sentry_pat
(** Precondition: concl has no existentials *)
- let map_auto (k,args) concl db =
+ let map_auto ~secvars (k,args) concl db =
let se = find k db in
let st = if db.use_dn then (Some db.hintdb_state) else None in
let pat = lookup_tacs concl st se in
- merge_entry db [] pat
+ merge_entry secvars db [] pat
- let map_existential (k,args) concl db =
+ let map_existential ~secvars (k,args) concl db =
let se = find k db in
if matches_modes args se.sentry_mode then
- merge_entry db se.sentry_nopat se.sentry_pat
- else merge_entry db [] []
+ merge_entry secvars db se.sentry_nopat se.sentry_pat
+ else merge_entry secvars db [] []
(* [c] contains an existential *)
- let map_eauto (k,args) concl db =
+ let map_eauto ~secvars (k,args) concl db =
let se = find k db in
if matches_modes args se.sentry_mode then
let st = if db.use_dn then Some db.hintdb_state else None in
let pat = lookup_tacs concl st se in
- merge_entry db [] pat
- else merge_entry db [] []
+ merge_entry secvars db [] pat
+ else merge_entry secvars db [] []
let is_exact = function
| Give_exact _ -> true
@@ -502,7 +589,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
@@ -567,11 +654,11 @@ module Hint_db = struct
let get_entry se =
let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in
- List.map realize_tac h
+ List.map snd h
let iter f db =
let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
- f None [] (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat);
+ f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
Constr_map.iter iter_se db.hintdb_map
let fold f db accu =
@@ -606,8 +693,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"
@@ -628,8 +713,7 @@ let searchtable_add (name,db) =
let current_db_names () = Hintdbmap.domain !searchtable
let current_db () = Hintdbmap.bindings !searchtable
-let current_pure_db () =
- List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
+let current_pure_db () = List.map snd (current_db ())
let error_no_such_hint_database x =
errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
@@ -669,7 +753,20 @@ let try_head_pattern c =
let with_uid c = { obj = c; uid = fresh_key () }
-let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
+let secvars_of_idset s =
+ Id.Set.fold (fun id p ->
+ if is_section_variable id then
+ Id.Pred.add id p
+ else p) s Id.Pred.empty
+
+let secvars_of_constr env c =
+ secvars_of_idset (global_vars_set env c)
+
+let secvars_of_global env gr =
+ secvars_of_idset (vars_of_global_reference env gr)
+
+let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
+ let secvars = secvars_of_constr env c in
let cty = strip_outer_cast cty in
match kind_of_term cty with
| Prod _ -> failwith "make_exact_entry"
@@ -679,14 +776,17 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
try head_pattern_bound pat
with BoundPattern -> failwith "make_exact_entry"
in
- (Some hd,
- { pri = (match pri with None -> 0 | Some p -> p);
- poly = poly;
- pat = Some pat;
- name = name;
- code = with_uid (Give_exact (c, cty, ctx)); })
+ let pri = match info.hint_priority with None -> 0 | Some p -> p in
+ let pat = match info.hint_pattern with
+ | Some pat -> snd pat
+ | None -> pat
+ in
+ (Some hd,
+ { pri; poly; pat = Some pat; name;
+ db = None; secvars;
+ code = with_uid (Give_exact (c, cty, ctx)); })
-let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
+let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) =
let cty = if hnf then hnf_constr env sigma cty else cty in
match kind_of_term cty with
| Prod _ ->
@@ -698,12 +798,16 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry" in
let nmiss = List.length (clenv_missing ce) in
+ let secvars = secvars_of_constr env c in
+ let pri = match info.hint_priority with None -> nb_hyp cty + nmiss | Some p -> p in
+ let pat = match info.hint_pattern with
+ | Some p -> snd p | None -> pat
+ in
if Int.equal nmiss 0 then
(Some hd,
- { pri = (match pri with None -> nb_hyp cty | Some p -> p);
- poly = poly;
- pat = Some pat;
- name = name;
+ { pri; poly; pat = Some pat; name;
+ db = None;
+ secvars;
code = with_uid (Res_pf(c,cty,ctx)); })
else begin
if not eapply then failwith "make_apply_entry";
@@ -711,10 +815,8 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++
str " will only be used by eauto");
(Some hd,
- { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
- poly = poly;
- pat = Some pat;
- name = name;
+ { pri; poly; pat = Some pat; name;
+ db = None; secvars;
code = with_uid (ERes_pf(c,cty,ctx)); })
end
| _ -> failwith "make_apply_entry"
@@ -765,13 +867,14 @@ let fresh_global_or_constr env sigma poly cr =
(c, Univ.ContextSet.empty)
end
-let make_resolves env sigma flags pri poly ?name cr =
+let make_resolves env sigma flags info poly ?name cr =
let c, ctx = fresh_global_or_constr env sigma poly cr in
let cty = Retyping.get_type_of env sigma c in
let try_apply f =
try Some (f (c, cty, ctx)) with Failure _ -> None in
let ents = List.map_filter try_apply
- [make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name]
+ [make_exact_entry env sigma info poly ?name;
+ make_apply_entry env sigma flags info poly ?name]
in
if List.is_empty ents then
errorlabstrm "Hint"
@@ -783,15 +886,17 @@ let make_resolves env sigma flags pri poly ?name cr =
(* used to add an hypothesis to the local hint database *)
let make_resolve_hyp env sigma decl =
let hname = get_id decl in
+ let c = mkVar hname in
try
- [make_apply_entry env sigma (true, true, false) None false
+ [make_apply_entry env sigma (true, true, false) empty_hint_info false
~name:(PathHints [VarRef hname])
- (mkVar hname, get_type decl, Univ.ContextSet.empty)]
+ (c, get_type decl, Univ.ContextSet.empty)]
with
| Failure _ -> []
| e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
(* REM : in most cases hintname = id *)
+
let make_unfold eref =
let g = global_of_evaluable_reference eref in
(Some g,
@@ -799,6 +904,8 @@ let make_unfold eref =
poly = false;
pat = None;
name = PathHints [g];
+ db = None;
+ secvars = secvars_of_global (Global.env ()) g;
code = with_uid (Unfold_nth eref) })
let make_extern pri pat tacast =
@@ -809,6 +916,8 @@ let make_extern pri pat tacast =
poly = false;
pat = pat;
name = PathAny;
+ db = None;
+ secvars = Id.Pred.empty; (* Approximation *)
code = with_uid (Extern tacast) })
let make_mode ref m =
@@ -832,6 +941,8 @@ 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;
+ secvars = secvars_of_constr env c;
code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
@@ -845,7 +956,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 +1016,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
@@ -1061,16 +1172,17 @@ let add_transparency l b local dbnames =
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_extern pri pat tacast local dbname =
- let pat = match pat with
+let add_extern info tacast local dbname =
+ let pat = match info.hint_pattern with
| None -> None
| Some (_, pat) -> Some pat
in
- let hint = make_hint ~local dbname (AddHints [make_extern pri pat tacast]) in
+ let hint = make_hint ~local dbname
+ (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
Lib.add_anonymous_leaf (inAutoHint hint)
-let add_externs pri pat tacast local dbnames =
- List.iter (add_extern pri pat tacast local) dbnames
+let add_externs info tacast local dbnames =
+ List.iter (add_extern info tacast local) dbnames
let add_trivials env sigma l local dbnames =
List.iter
@@ -1084,15 +1196,16 @@ let (forward_intern_tac, extern_intern_tac) = Hook.make ()
type hnf = bool
+type hint_info = (patvar list * constr_pattern) hint_info_gen
+
type hints_entry =
- | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list
+ | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
| HintsModeEntry of global_reference * hint_mode list
- | HintsExternEntry of
- int * (patvar list * constr_pattern) option * glob_tactic_expr
+ | HintsExternEntry of hint_info * glob_tactic_expr
let default_prepare_hint_ident = Id.of_string "H"
@@ -1156,11 +1269,12 @@ let interp_hints poly =
(PathHints [gr], poly, IsGlobRef gr)
| HintsConstr c -> (PathAny, poly, f poly c)
in
- let fres (pri, b, r) =
+ let fp = Constrintern.intern_constr_pattern (Global.env()) in
+ let fres (info, b, r) =
let path, poly, gr = fi r in
- (pri, poly, b, path, gr)
+ let info = { info with hint_pattern = Option.map fp info.hint_pattern } in
+ (info, poly, b, path, gr)
in
- let fp = Constrintern.intern_constr_pattern (Global.env()) in
match h with
| HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
| HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
@@ -1176,14 +1290,14 @@ let interp_hints poly =
List.init (nconstructors ind)
(fun i -> let c = (ind,i+1) in
let gr = ConstructRef c in
- None, mib.Declarations.mind_polymorphic, true,
+ empty_hint_info, mib.Declarations.mind_polymorphic, true,
PathHints [gr], IsGlobRef gr)
in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
| HintsExtern (pri, patcom, tacexp) ->
let pat = Option.map fp patcom in
let l = match pat with None -> [] | Some (l, _) -> l in
let tacexp = Hook.get forward_intern_tac l tacexp in
- HintsExternEntry (pri, pat, tacexp)
+ HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
let add_hints local dbnames0 h =
if String.List.mem "nocore" dbnames0 then
@@ -1199,8 +1313,8 @@ let add_hints local dbnames0 h =
| HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
| HintsTransparencyEntry (lhints, b) ->
add_transparency lhints b local dbnames
- | HintsExternEntry (pri, pat, tacexp) ->
- add_externs pri pat tacexp local dbnames
+ | HintsExternEntry (info, tacexp) ->
+ add_externs info tacexp local dbnames
let expand_constructor_hints env sigma lems =
List.map_append (fun (evd,lem) ->
@@ -1224,7 +1338,7 @@ let add_hint_lemmas env sigma eapply lems hint_db =
let lems = expand_constructor_hints env sigma lems in
let hintlist' =
List.map_append (fun (poly, lem) ->
- make_resolves env sigma (eapply,true,false) None poly lem) lems in
+ make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in
Hint_db.add_list env sigma hintlist' hint_db
let make_local_hint_db env sigma ts eapply lems =
@@ -1262,11 +1376,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 =
@@ -1278,7 +1392,9 @@ let pr_hint h = match h.obj with
(str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
let pr_id_hint (id, v) =
- (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
+ let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in
+ (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
+ ++ str", id " ++ int id ++ str ")" ++ spc ())
let pr_hint_list hintlist =
(str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
@@ -1292,7 +1408,7 @@ let pr_hints_db (name,db,hintlist) =
let pr_hint_list_for_head c =
let dbs = current_db () in
let validate (name, db) =
- let hints = List.map (fun v -> 0, v) (Hint_db.map_all c db) in
+ let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in
(name, db, hints)
in
let valid_dbs = List.map validate dbs in
@@ -1314,9 +1430,9 @@ let pr_hint_term cl =
let fn = try
let hdc = decompose_app_bound cl in
if occur_existential cl then
- Hint_db.map_existential hdc cl
- else Hint_db.map_auto hdc cl
- with Bound -> Hint_db.map_none
+ Hint_db.map_existential ~secvars:Id.Pred.full hdc cl
+ else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl
+ with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
in
let fn db = List.map (fun x -> 0, x) (fn db) in
List.map (fun (name, db) -> (name, db, fn db)) dbs
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 6f5ee8ba5e..1be3e0c52f 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -25,6 +25,10 @@ exception Bound
val decompose_app_bound : constr -> global_reference * constr array
+val secvars_of_hyps : Context.Named.t -> Id.Pred.t
+
+val empty_hint_info : 'a hint_info_gen
+
(** Pre-created hint databases *)
type 'a hint_ast =
@@ -38,17 +42,22 @@ type 'a hint_ast =
type hint
type raw_hint = constr * types * Univ.universe_context_set
-type hints_path_atom =
- | PathHints of global_reference list
+type 'a hints_path_atom_gen =
+ | PathHints of 'a list
(* For forward hints, their names is the list of projections *)
| PathAny
+type hints_path_atom = global_reference hints_path_atom_gen
+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 *)
- code : 'a; (** the tactic to apply when the concl matches pat *)
+ db : hint_db_name option;
+ secvars : Id.Pred.t; (** The section variables this hint depends on, as a predicate *)
+ code : 'a; (** the tactic to apply when the concl matches pat *)
}
type full_hint = hint with_metadata
@@ -59,42 +68,56 @@ type search_entry
type hint_entry
-type hints_path =
- | PathAtom of hints_path_atom
- | PathStar of hints_path
- | PathSeq of hints_path * hints_path
- | PathOr of hints_path * hints_path
+type 'a hints_path_gen =
+ | PathAtom of 'a hints_path_atom_gen
+ | PathStar of 'a hints_path_gen
+ | PathSeq of 'a hints_path_gen * 'a hints_path_gen
+ | PathOr of 'a hints_path_gen * 'a hints_path_gen
| PathEmpty
| PathEpsilon
+type pre_hints_path = Libnames.reference hints_path_gen
+type hints_path = global_reference hints_path_gen
+
val normalize_path : hints_path -> hints_path
val path_matches : hints_path -> hints_path_atom list -> bool
val path_derivate : hints_path -> hints_path_atom -> hints_path
-val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds
+val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds
+val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds
val pp_hints_path : hints_path -> Pp.std_ppcmds
val pp_hint_mode : hint_mode -> Pp.std_ppcmds
+val glob_hints_path_atom :
+ Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
+val glob_hints_path :
+ Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen
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
+
+ (** All hints which have no pattern.
+ * [secvars] represent the set of section variables that
+ * can be used in the hint. *)
+ val map_none : secvars:Id.Pred.t -> t -> full_hint list
(** All hints associated to the reference *)
- val map_all : global_reference -> t -> full_hint list
+ val map_all : secvars:Id.Pred.t -> global_reference -> 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 : (global_reference * constr array) -> constr -> t -> full_hint list
+ val map_existential : secvars:Id.Pred.t ->
+ (global_reference * 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 : (global_reference * constr array) -> constr -> t -> full_hint list
+ val map_eauto : secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments. *)
- val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
+ val map_auto : secvars:Id.Pred.t ->
+ (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
@@ -113,26 +136,25 @@ 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
+type hint_info = (patvar list * constr_pattern) hint_info_gen
+
type hint_term =
| IsGlobRef of global_reference
| IsConstr of constr * Univ.universe_context_set
type hints_entry =
- | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom *
- hint_term) list
+ | HintsResolveEntry of
+ (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
| HintsModeEntry of global_reference * hint_mode list
- | HintsExternEntry of
- int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
+ | HintsExternEntry of hint_info * Tacexpr.glob_tactic_expr
val searchtable_map : hint_db_name -> hint_db
@@ -159,22 +181,34 @@ val prepare_hint : bool (* Check no remaining evars *) ->
(bool * bool) (* polymorphic or monomorphic, local or global *) ->
env -> evar_map -> open_constr -> hint_term
-(** [make_exact_entry pri (c, ctyp)].
+(** [make_exact_entry info (c, ctyp, ctx)].
[c] is the term given as an exact proof to solve the goal;
- [ctyp] is the type of [c]. *)
-
-val make_exact_entry : env -> evar_map -> int option -> polymorphic -> ?name:hints_path_atom ->
+ [ctyp] is the type of [c].
+ [ctx] is its (refreshable) universe context.
+ In info:
+ [hint_priority] is the hint's desired priority, it is 0 if unspecified
+ [hint_pattern] is the hint's desired pattern, it is inferred if not specified
+*)
+
+val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom ->
(constr * types * Univ.universe_context_set) -> hint_entry
-(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)].
+(** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
[eapply] is true if this hint will be used only with EApply;
[hnf] should be true if we should expand the head of cty before searching for
products;
[c] is the term given as an exact proof to solve the goal;
- [cty] is the type of [c]. *)
+ [cty] is the type of [c].
+ [ctx] is its (refreshable) universe context.
+ In info:
+ [hint_priority] is the hint's desired priority, it is computed as the number of products in [cty]
+ if unspecified
+ [hint_pattern] is the hint's desired pattern, it is inferred from the conclusion of [cty]
+ if not specified
+*)
val make_apply_entry :
- env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom ->
+ env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
(constr * types * Univ.universe_context_set) -> hint_entry
(** A constr which is Hint'ed will be:
@@ -185,7 +219,7 @@ val make_apply_entry :
has missing arguments. *)
val make_resolves :
- env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom ->
+ env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
hint_term -> hint_entry list
(** [make_resolve_hyp hname htyp].
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..9d64e7c599 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
@@ -79,7 +83,7 @@ let _ =
let apply_solve_class_goals = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optsync = true; Goptions.optdepr = true;
Goptions.optname =
"Perform typeclass resolution on apply-generated subgoals.";
Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"];
@@ -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
@@ -1137,7 +1141,7 @@ let run_delayed env sigma c =
let tactic_infer_flags with_evar = {
Pretyping.use_typeclasses = true;
- Pretyping.use_unif_heuristics = true;
+ Pretyping.solve_unification_constraints = true;
Pretyping.use_hook = Some solve_by_implicit_tactic;
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true }
@@ -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 ->
@@ -2712,7 +2714,7 @@ let forward b usetac ipat c =
match usetac with
| None ->
Proofview.Goal.enter { enter = begin fun gl ->
- let t = Tacmach.New.pf_unsafe_type_of gl c in
+ let t = Tacmach.New.pf_get_type_of gl c in
let hd = head_ident c in
Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
end }
@@ -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
@@ -4967,9 +4973,16 @@ module New = struct
open Locus
let reduce_after_refine =
+ let onhyps =
+ (** We reduced everywhere in the hyps before 8.6 *)
+ if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0
+ then None
+ else Some []
+ in
reduce
- (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]})
- {onhyps=Some []; concl_occs=AllOccurrences }
+ (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;
+ rZeta=false;rDelta=false;rConst=[]})
+ {onhyps; concl_occs=AllOccurrences }
let refine ?unsafe c =
Refine.refine ?unsafe c <*>
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 00:42:05 +0000