diff options
| author | Emilio Jesus Gallego Arias | 2020-04-02 03:51:12 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-15 11:12:36 -0400 |
| commit | 4a9d1b4b190e2cb3fb034882a703aa54c5059035 (patch) | |
| tree | 734ee679cd83e6aeab7855714532307d2e8d79d9 | |
| parent | 29314bb99b5b93f619d9cc68cb3b6dbcae1942cb (diff) | |
[proofs] Move pfedit to `proofs`
It seems to belong there, not in `tactics`
| -rw-r--r-- | proofs/pfedit.ml (renamed from tactics/pfedit.ml) | 0 | ||||
| -rw-r--r-- | proofs/pfedit.mli (renamed from tactics/pfedit.mli) | 0 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 1 |
4 files changed, 1 insertions, 1 deletions
diff --git a/tactics/pfedit.ml b/proofs/pfedit.ml index 20975cbc57..20975cbc57 100644 --- a/tactics/pfedit.ml +++ b/proofs/pfedit.ml diff --git a/tactics/pfedit.mli b/proofs/pfedit.mli index 8d06a260da..8d06a260da 100644 --- a/tactics/pfedit.mli +++ b/proofs/pfedit.mli diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 756fef0511..91e1ee22aa 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -6,6 +6,7 @@ Proof Logic Goal_select Proof_bullet +Pfedit Refiner Tacmach Clenv diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index d1865c974c..537d111f23 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,5 +1,4 @@ DeclareScheme -Pfedit Declare Dnet Dn |