diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-26 11:41:46 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-26 11:41:46 +0000 |
| commit | e81cf0fed810f8d4498359502d3623661c62050e (patch) | |
| tree | 5282bd59ae512ca92ab01b16e938740fbb77408b /translate/pptacticnew.ml | |
| parent | d926a11a23fd6fae8bfec9e8b163c1a83ac33ebf (diff) | |
Ajout now_show
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4487 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate/pptacticnew.ml')
| -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 574b66501..335160f6b 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 = |