aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--interp/discharge.ml (renamed from vernac/discharge.ml)0
-rw-r--r--interp/discharge.mli (renamed from vernac/discharge.mli)0
2 files changed, 0 insertions, 0 deletions
diff --git a/vernac/discharge.ml b/interp/discharge.ml
index 0e4bbd2993..0e4bbd2993 100644
--- a/vernac/discharge.ml
+++ b/interp/discharge.ml
diff --git a/vernac/discharge.mli b/interp/discharge.mli
index c8c7e3b8b8..c8c7e3b8b8 100644
--- a/vernac/discharge.mli
+++ b/interp/discharge.mli