diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-25 14:24:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-25 14:25:58 +0100 |
| commit | e8114ee084cae195eb7615293cec0e28dcc0a3d8 (patch) | |
| tree | 6cc1208059a78d1f85042467542d35871120f831 | |
| parent | 222c24ff4361f1a35b267f6b406aa7b2da56e689 (diff) | |
Moving Autorewrite back to tactics/.
| -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 28bfa5aa0..e0c6f3ac0 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 4816f8a45..4816f8a45 100644 --- a/ltac/autorewrite.ml +++ b/tactics/autorewrite.ml diff --git a/ltac/autorewrite.mli b/tactics/autorewrite.mli index ac613b57c..ac613b57c 100644 --- a/ltac/autorewrite.mli +++ b/tactics/autorewrite.mli diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 37503decc..ab8069225 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -22,3 +22,4 @@ Class_tactics Tactic_matching Term_dnet Eqdecide +Autorewrite |