diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 3 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 14 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 |
5 files changed, 11 insertions, 12 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 0931c3e61e..488bcb5208 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -369,8 +369,7 @@ and tac_of_hint dbg db_list local_db concl (flags, h) = let info = Exninfo.reify () in Tacticals.New.tclFAIL ~info 0 (str"Unbound reference") end - | Extern tacast -> - let p = FullHint.pattern h in + | Extern (p, tacast) -> conclPattern concl p tacast in let pr_hint env sigma = diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 36544883aa..378a3e718b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -359,7 +359,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm Tacticals.New.tclTHEN fst snd | Unfold_nth c -> Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c]) - | Extern tacast -> conclPattern concl p tacast + | Extern (p, tacast) -> conclPattern concl p tacast in let tac = FullHint.run h tac in let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 9a554b117e..17e6a6edb4 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -126,7 +126,7 @@ and e_my_find_search env sigma db_list local_db secvars concl = Tacticals.New.tclTHEN (unify_e_resolve st h) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl - | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast + | Extern (pat, tacast) -> conclPattern concl pat tacast in let tac = FullHint.run h tac in (tac, b, lazy (FullHint.print env sigma h)) diff --git a/tactics/hints.ml b/tactics/hints.ml index 0ab1adda4b..0b11c1e79f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -105,7 +105,7 @@ type 'a hint_ast = | Give_exact of 'a | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *) | Unfold_nth of evaluable_global_reference (* Hint Unfold *) - | Extern of Genarg.glob_generic_argument (* Hint Extern *) + | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *) type 'a hints_path_atom_gen = @@ -349,8 +349,7 @@ let instantiate_hint env sigma p = | Res_pf_THEN_trivial_fail c -> Res_pf_THEN_trivial_fail (mk_clenv c) | Give_exact c -> Give_exact (mk_clenv c) - | Unfold_nth e -> Unfold_nth e - | Extern t -> Extern t + | (Unfold_nth _ | Extern _) as h -> h in { p with code = { p.code with obj = code } } @@ -969,7 +968,7 @@ let make_extern pri pat tacast = name = PathAny; db = None; secvars = Id.Pred.empty; (* Approximation *) - code = with_uid (Extern tacast) }) + code = with_uid (Extern (pat, tacast)) }) let make_mode ref m = let open Term in @@ -1133,9 +1132,10 @@ let subst_autohint (subst, obj) = | Unfold_nth ref -> let ref' = subst_evaluable_reference subst ref in if ref==ref' then data.code.obj else Unfold_nth ref' - | Extern tac -> + | Extern (pat, tac) -> + let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in let tac' = Genintern.generic_substitute subst tac in - if tac==tac' then data.code.obj else Extern tac' + if pat==pat' && tac==tac' then data.code.obj else Extern (pat', tac') in let name' = subst_path_atom subst data.name in let uid' = subst_kn subst data.code.uid in @@ -1415,7 +1415,7 @@ let pr_hint env sigma h = match h.obj with (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") | Unfold_nth c -> str"unfold " ++ pr_evaluable_reference c - | Extern tac -> + | Extern (_, tac) -> str "(*external*) " ++ Pputils.pr_glb_generic env sigma tac let pr_id_hint env sigma (id, v) = diff --git a/tactics/hints.mli b/tactics/hints.mli index f0fed75828..0b9da27ab3 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -37,7 +37,7 @@ type 'a hint_ast = | Give_exact of 'a | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *) | Unfold_nth of evaluable_global_reference (* Hint Unfold *) - | Extern of Genarg.glob_generic_argument (* Hint Extern *) + | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *) type hint = private { hint_term : constr; |