From 21b4e41544f03de18d9f5b1bdb93a26b36a97999 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Jun 2020 15:17:33 +0200 Subject: Opacify the type of hint metadata. --- tactics/eauto.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'tactics/eauto.ml') diff --git a/tactics/eauto.ml b/tactics/eauto.ml index c2eabffd44..7a141bb53b 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -120,10 +120,11 @@ and e_my_find_search env sigma db_list local_db secvars concl = List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list) in let tac_of_hint = - fun (st, {pri = b; pat = p; code = t; poly = poly}) -> - let b = match Hints.repr_hint t with + fun (st, h) -> + let poly = FullHint.is_polymorphic h in + let b = match FullHint.repr h with | Unfold_nth _ -> 1 - | _ -> b + | _ -> FullHint.priority h in let tac = function | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl) @@ -133,10 +134,10 @@ and e_my_find_search env sigma db_list local_db secvars concl = Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl)) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl - | Extern tacast -> conclPattern concl p tacast + | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast in - let tac = run_hint t tac in - (tac, b, lazy (pr_hint env sigma t)) + let tac = FullHint.run h tac in + (tac, b, lazy (FullHint.print env sigma h)) in List.map tac_of_hint hintl -- cgit v1.2.3 From 9eca7cca68dc82aa738a8d408d75e1b9b5405646 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Jun 2020 18:57:25 +0200 Subject: Wrap the content of full hints into a record. --- tactics/eauto.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'tactics/eauto.ml') diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 7a141bb53b..4a6364795b 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -65,9 +65,9 @@ open Auto (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) (***************************************************************************) -let unify_e_resolve poly flags (c,clenv) = +let unify_e_resolve poly flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv ~poly c clenv gl in + let clenv', c = connect_hint_clenv ~poly h gl in let clenv' = clenv_unique_resolver ~flags clenv' gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) @@ -88,9 +88,9 @@ let hintmap_of sigma secvars concl = else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) -let e_exact poly flags (c,clenv) = +let e_exact poly flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv ~poly c clenv gl in + let clenv', c = connect_hint_clenv ~poly h gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (e_give_exact c) @@ -127,11 +127,11 @@ and e_my_find_search env sigma db_list local_db secvars concl = | _ -> FullHint.priority h in let tac = function - | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl) - | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) - | Give_exact (c,cl) -> e_exact poly st (c,cl) - | Res_pf_THEN_trivial_fail (term,cl) -> - Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl)) + | Res_pf h -> unify_resolve ~poly st h + | ERes_pf h -> unify_e_resolve poly st h + | Give_exact h -> e_exact poly st h + | Res_pf_THEN_trivial_fail h -> + Tacticals.New.tclTHEN (unify_e_resolve poly 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 -- cgit v1.2.3 From c00a369a8bd70efad3e1481daa78ab483038c6cb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Jun 2020 19:20:02 +0200 Subject: Move the hint polymorphic status to the hint instance. It is only used for this kind of hints, never for Extern / Unfold. --- tactics/eauto.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) (limited to 'tactics/eauto.ml') diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 4a6364795b..0ff90bc046 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -65,9 +65,9 @@ open Auto (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) (***************************************************************************) -let unify_e_resolve poly flags h = +let unify_e_resolve flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv ~poly h gl in + let clenv', c = connect_hint_clenv h gl in let clenv' = clenv_unique_resolver ~flags clenv' gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) @@ -88,9 +88,9 @@ let hintmap_of sigma secvars concl = else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) -let e_exact poly flags h = +let e_exact flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv ~poly h gl in + let clenv', c = connect_hint_clenv h gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (e_give_exact c) @@ -121,17 +121,16 @@ and e_my_find_search env sigma db_list local_db secvars concl = in let tac_of_hint = fun (st, h) -> - let poly = FullHint.is_polymorphic h in let b = match FullHint.repr h with | Unfold_nth _ -> 1 | _ -> FullHint.priority h in let tac = function - | Res_pf h -> unify_resolve ~poly st h - | ERes_pf h -> unify_e_resolve poly st h - | Give_exact h -> e_exact poly st h + | Res_pf h -> unify_resolve st h + | ERes_pf h -> unify_e_resolve st h + | Give_exact h -> e_exact st h | Res_pf_THEN_trivial_fail h -> - Tacticals.New.tclTHEN (unify_e_resolve poly st h) + 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 -- cgit v1.2.3