aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorgareuselesinge2013-10-31 14:24:43 +0000
committergareuselesinge2013-10-31 14:24:43 +0000
commitdbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e (patch)
treef09931dac187ca9b20bb483aee7bc9beca1e78f1 /dev
parentb0631cba10fda88eb3518153860807b10441ef34 (diff)
Conv_orable made functional and part of pre_env
But for vm, the kernel should be functional now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
-rw-r--r--dev/printers.mllib2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 1fc249eef5..c14d72def1 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -60,13 +60,13 @@ Future
Lazyconstr
Declareops
Retroknowledge
+Conv_oracle
Pre_env
Nativelambda
Nativecode
Nativelib
Cbytegen
Environ
-Conv_oracle
Closure
Reduction
Nativeconv