aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/g_obligations.ml4 (renamed from parsing/g_obligations.ml4)0
1 files changed, 0 insertions, 0 deletions
diff --git a/parsing/g_obligations.ml4 b/toplevel/g_obligations.ml4
index 2354aa3325..2354aa3325 100644
--- a/parsing/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4