diff options
| -rw-r--r-- | translate/pptacticnew.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 574b665019..335160f6b4 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -112,6 +112,7 @@ let translate_v7_ltac = function | "SimplMonom" -> "simpl_monom" | "SimplAllMonoms" -> "simpl_all_monomials" | "AssocDistrib" -> "assoc_distrib" + | "NowShow" -> "now_show" | x -> x let id_of_ltac_v7_id id = |