diff options
| author | Pierre-Marie Pédrot | 2016-03-21 09:59:52 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-25 13:37:03 +0100 |
| commit | 63b914b51ddc9084bc2e059df266e2345dfe34b5 (patch) | |
| tree | 95c7069a50169c76eefbcf4cb014fdafa104bb18 | |
| parent | a947e85e88ab0b9a5a4cfea81ecbeec6f52636ea (diff) | |
Moving Eqdecide to tactics/.
| -rw-r--r-- | ltac/ltac.mllib | 1 | ||||
| -rw-r--r-- | tactics/eqdecide.ml (renamed from ltac/eqdecide.ml) | 0 | ||||
| -rw-r--r-- | tactics/eqdecide.mli (renamed from ltac/eqdecide.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 8e9f992f16..28bfa5aa0a 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -16,6 +16,5 @@ G_class Rewrite G_rewrite Tauto -Eqdecide G_eqdecide G_ltac diff --git a/ltac/eqdecide.ml b/tactics/eqdecide.ml index 011296a8d0..011296a8d0 100644 --- a/ltac/eqdecide.ml +++ b/tactics/eqdecide.ml diff --git a/ltac/eqdecide.mli b/tactics/eqdecide.mli index cb48a5bcc8..cb48a5bcc8 100644 --- a/ltac/eqdecide.mli +++ b/tactics/eqdecide.mli diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index bbad1d8e64..37503decc6 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -21,3 +21,4 @@ Eauto Class_tactics Tactic_matching Term_dnet +Eqdecide |