aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-26 17:31:10 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-26 17:31:10 +0000
commit0699ef2ffba984e7b7552787894b142dd924f66a (patch)
treef67f2842cc12c523b620663ce23840bf6a411338
parent0919391f43729bf172ab00c8dec9438a0a9f59ab (diff)
Moved Entries module back to kernel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15931 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--kernel/entries.mli (renamed from intf/entries.mli)0
1 files changed, 0 insertions, 0 deletions
diff --git a/intf/entries.mli b/kernel/entries.mli
index 2460ec644..2460ec644 100644
--- a/intf/entries.mli
+++ b/kernel/entries.mli