diff options
| -rw-r--r-- | ltac/ltac.mllib | 1 | ||||
| -rw-r--r-- | tactics/autorewrite.ml (renamed from ltac/autorewrite.ml) | 0 | ||||
| -rw-r--r-- | tactics/autorewrite.mli (renamed from ltac/autorewrite.mli) | 0 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 1 |
4 files changed, 1 insertions, 1 deletions
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index 28bfa5aa0a..e0c6f3ac0a 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -9,7 +9,6 @@ Tactic_option Extraargs G_obligations Coretactics -Autorewrite Extratactics G_auto G_class diff --git a/ltac/autorewrite.ml b/tactics/autorewrite.ml index 4816f8a452..4816f8a452 100644 --- a/ltac/autorewrite.ml +++ b/tactics/autorewrite.ml diff --git a/ltac/autorewrite.mli b/tactics/autorewrite.mli index ac613b57ce..ac613b57ce 100644 --- a/ltac/autorewrite.mli +++ b/tactics/autorewrite.mli diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 37503decc6..ab8069225d 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -22,3 +22,4 @@ Class_tactics Tactic_matching Term_dnet Eqdecide +Autorewrite |