aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/extraction.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-12 16:32:43 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-12 16:32:43 +0000
commit3725135942a9778cbc741602dc6ecba23dde46f8 (patch)
treef3f211d705bc64eaeb003c4f216d3d8fc339e348 /contrib/extraction/extraction.mli
parent1de518f08e3213e2b68cfb3aa425fc7247942d92 (diff)
nouvelle gestion des variables de type ML
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1583 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/extraction.mli')
-rw-r--r--contrib/extraction/extraction.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 0f08f3128..e75e39fe6 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -23,7 +23,7 @@ type arity = Arity | NotArity
type type_var = info * arity
-type signature = (type_var * identifier) list
+type signature = type_var list
type extraction_context = bool list