feat(library/tactic/simplify): load options on simplifier entry (#456)

This allows the creation of a `simp?` tactic that locally enables
the `simplify.trace.rewrite` option.

src/library/tactic/simplify.cpp

@@ -1245,6 +1245,7 @@ meta constant simplify
 vm_obj tactic_simplify(vm_obj const & slss, vm_obj const & u, vm_obj const & e, vm_obj const & c, vm_obj const & rel,
                        vm_obj const & prove, vm_obj const & _s) {
     tactic_state s0 = tactic::to_state(_s);
+    scope_trace_env env(s0.get_options());
     auto s = freeze_local_instances(s0);
     bool was_frozen = is_eqp(s, s0);
     try {

tests/lean/simp_trace.lean

@@ -0,0 +1,15 @@
+-- Options (particularly trace options) are refreshed
+-- upon entry to the simplifier.
+
+example {p : Prop} (h : p) : p :=
+begin
+  have h₁ : true = true := rfl,
+  have h₂ : true = true := rfl,
+  have h₃ : true = true := rfl,
+  simp at h₁,
+  tactic.set_bool_option `trace.simplify.rewrite tt,
+  simp at h₂,
+  tactic.set_bool_option `pp.all tt,
+  simp at h₃,
+  exact h
+end

tests/lean/simp_trace.lean.expected.out

@@ -0,0 +1,2 @@
+0. [simplify.rewrite] [eq_self_iff_true]: true = true ==> true
+0. [simplify.rewrite] [eq_self_iff_true]: @eq.{1} Prop true true ==> true