aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/ocaml.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-12-18 13:57:49 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-12-18 13:57:49 +0000
commit1a61af5ad0da102f6912ce3c7a18fe4770f23be4 (patch)
tree8ff10cf3cef8cf2cd90e807065e2205821bb9373 /contrib/extraction/ocaml.mli
parentdae8ca4c57bd9c450b734a6b7cac985a03b30eef (diff)
typo de parenthèsage + suppression de string (= str maintenant)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/ocaml.mli')
-rw-r--r--contrib/extraction/ocaml.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index e9faa1a0a..3c3934836 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -20,7 +20,6 @@ val current_module : identifier option ref
val collapse_type_app : ml_type list -> ml_type list
-val string : string -> std_ppcmds
val open_par : bool -> std_ppcmds
val close_par : bool -> std_ppcmds
val pp_abst : identifier list -> std_ppcmds