aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/pattern.ml (renamed from proofs/pattern.ml)0
-rw-r--r--parsing/pattern.mli (renamed from proofs/pattern.mli)0
2 files changed, 0 insertions, 0 deletions
diff --git a/proofs/pattern.ml b/parsing/pattern.ml
index 6d3c362d68..6d3c362d68 100644
--- a/proofs/pattern.ml
+++ b/parsing/pattern.ml
diff --git a/proofs/pattern.mli b/parsing/pattern.mli
index b725d90446..b725d90446 100644
--- a/proofs/pattern.mli
+++ b/parsing/pattern.mli