aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/scheme.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-28 02:27:12 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-28 02:27:12 +0000
commit41caeae1003a24dd623aabe2907940d3151f1151 (patch)
treec0cabb60d5d06e01e2cf693462bf30ce9062a9ca /contrib/extraction/scheme.mli
parent23931fef8a21e5bff5c1faa7d9d9dd6787197d35 (diff)
Reorganisation du pretty-print:
- Dfix sans rename_global - question du renommage - code cleanup (plein) Encore a finir: bug modules/qualification et syntax records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3321 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/scheme.mli')
-rw-r--r--contrib/extraction/scheme.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 51fac4fb7..f39afd34f 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -17,7 +17,8 @@ open Nametab
val keywords : Idset.t
-val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
+val preamble :
+ extraction_params -> identifier list -> bool * bool * bool -> std_ppcmds
module Make : functor(P : Mlpp_param) -> Mlpp