diff options
author | 2001-11-14 13:36:50 +0000 | |
---|---|---|
committer | 2001-11-14 13:36:50 +0000 | |
commit | 5a02d3ad27b799531d3cb9acc6bdee655c89a372 (patch) | |
tree | 3ce220108d4d7aeddfdffda2802afc3cb78390c2 /contrib/extraction/extraction.mli | |
parent | e3f8244e98bf312539c14f1eacc07b33201c48e1 (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.mli | 2 |
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 |