aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/extraction.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-11-14 13:36:50 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-11-14 13:36:50 +0000
commit5a02d3ad27b799531d3cb9acc6bdee655c89a372 (patch)
tree3ce220108d4d7aeddfdffda2802afc3cb78390c2 /contrib/extraction/extraction.mli
parente3f8244e98bf312539c14f1eacc07b33201c48e1 (diff)
Revolution culturelle: suppression des arguments prop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2189 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/extraction.mli')
-rw-r--r--contrib/extraction/extraction.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 3f71c1d89..39f8d08b7 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -37,5 +37,3 @@ val extract_constr : env -> constr -> extraction_result
(*s ML declaration corresponding to a Coq reference. *)
val extract_declaration : global_reference -> ml_decl
-
-val signature : env -> constr -> signature