Merge remote-tracking branch 'origin/master'

lecopivo · Mar 9, 2024 · 3cc8c3e · 3cc8c3e
2 parents 914eee2 + bbd3a39
commit 3cc8c3e
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/SciLean/Tactic/Autodiff.lean b/SciLean/Tactic/Autodiff.lean
@@ -15,7 +15,9 @@ simproc_decl lift_lets_simproc (_) := fun e => do
 
 -- todo: add option, discharger, only and [...] syntax
 macro "autodiff" : conv =>
-  `(conv| fun_trans (config:={zeta:=false,singlePass:=true}) (disch:=sorry) only [ftrans_simp,lift_lets_simproc])
+  `(conv| (fun_trans (config:={zeta:=false,singlePass:=true}) (disch:=sorry) only [ftrans_simp,lift_lets_simproc];
+           simp (config:={zeta:=false,failIfUnchanged:=false}) only [ftrans_simp,lift_lets_simproc]))
 
 macro "autodiff" : tactic =>
-  `(tactic| fun_trans (config:={zeta:=false,singlePass:=true}) (disch:=sorry) only [ftrans_simp,lift_lets_simproc])
+  `(tactic| (fun_trans (config:={zeta:=false,singlePass:=true}) (disch:=sorry) only [ftrans_simp,lift_lets_simproc];
+             simp (config:={zeta:=false,failIfUnchanged:=false}) only [ftrans_simp,lift_lets_simproc]))