diff options
| -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 |