aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/table.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-12-09 02:27:09 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-12-09 02:27:09 +0000
commitdf848afcfaf69a7b132dea824f0cd1602898ea60 (patch)
tree0a1ada8f4dcdb4dadc5bf6ae37fab7c2d34ccfcd /contrib/extraction/table.mli
parent69269d594e4bda8ac18127e893b97c02fb6f0961 (diff)
travail sur les types extraits
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6441 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/table.mli')
-rw-r--r--contrib/extraction/table.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 0b69a7412..6be869e59 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -71,6 +71,10 @@ val reset_tables : unit -> unit
val auto_inline : unit -> bool
+(*s TypeExpand parameter *)
+
+val type_expand : unit -> bool
+
(*s Optimize parameter *)
type opt_flag =