diff options
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 9 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 1 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 7 | ||||
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/2417.v | 15 | ||||
| -rw-r--r-- | test-suite/success/hintdb_in_ltac.v | 14 | ||||
| -rw-r--r-- | test-suite/success/hintdb_in_ltac_bis.v | 15 |
7 files changed, 50 insertions, 12 deletions
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index a37cf306e..4ec42c676 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -149,15 +149,6 @@ TACTIC EXTEND autounfold_one [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ] END -TACTIC EXTEND autounfoldify -| [ "autounfoldify" constr(x) ] -> [ - let db = match Term.kind_of_term x with - | Term.Const (c,_) -> Names.Label.to_string (Names.con_label c) - | _ -> assert false - in Eauto.autounfold ["core";db] Locusops.onConcl - ] -END - TACTIC EXTEND unify | ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ] | ["unify" constr(x) constr(y) "with" preident(base) ] -> [ diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 763e0dc22..4b5d87fc3 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -782,6 +782,7 @@ let intern_ltac ist tac = let () = Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); Genintern.register_intern0 wit_ref (lift intern_global_reference); + Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; Genintern.register_intern0 wit_var (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 32bcdfb6a..fda9142ed 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2023,9 +2023,6 @@ let () = let () = declare_uniform wit_string -let () = - declare_uniform wit_pre_ident - let lift f = (); fun ist x -> Ftactic.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in @@ -2053,9 +2050,13 @@ let interp_destruction_arg' ist c = Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (interp_destruction_arg ist gl c) end } +let interp_pre_ident ist env sigma s = + s |> Id.of_string |> interp_ident ist env sigma |> Id.to_string + let () = register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); register_interp0 wit_ref (lift interp_reference); + register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); register_interp0 wit_var (lift interp_hyp); register_interp0 wit_intro_pattern (lifts interp_intro_pattern); diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 55de58361..b09bdda65 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -291,6 +291,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) = let () = Genintern.register_subst0 wit_int_or_var (fun _ v -> v); Genintern.register_subst0 wit_ref subst_global_reference; + Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); Genintern.register_subst0 wit_var (fun _ v -> v); Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v new file mode 100644 index 000000000..b2f00ffc6 --- /dev/null +++ b/test-suite/bugs/closed/2417.v @@ -0,0 +1,15 @@ +Parameter x y : nat. +Axiom H : x = y. +Hint Rewrite H : mybase. + +Ltac bar base := autorewrite with base. + +Tactic Notation "foo" ident(base) := autorewrite with base. + +Goal x = 0. + bar mybase. + now_show (y = 0). + Undo 2. + foo mybase. + now_show (y = 0). +Abort. diff --git a/test-suite/success/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v new file mode 100644 index 000000000..f12b4d1f4 --- /dev/null +++ b/test-suite/success/hintdb_in_ltac.v @@ -0,0 +1,14 @@ +Definition x := 0. + +Hint Unfold x : mybase. + +Ltac autounfoldify base := autounfold with base. + +Tactic Notation "autounfoldify_bis" ident(base) := autounfold with base. + +Goal x = 0. + progress autounfoldify mybase. + Undo. + progress autounfoldify_bis mybase. + trivial. +Qed. diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v new file mode 100644 index 000000000..f5c25540e --- /dev/null +++ b/test-suite/success/hintdb_in_ltac_bis.v @@ -0,0 +1,15 @@ +Parameter Foo : Prop. +Axiom H : Foo. + +Hint Resolve H : mybase. + +Ltac foo base := eauto with base. + +Tactic Notation "bar" ident(base) := + typeclasses eauto with base. + +Goal Foo. + progress foo mybase. + Undo. + progress bar mybase. +Qed.
\ No newline at end of file |