aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/ocaml.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-04-20 09:57:01 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-04-20 09:57:01 +0000
commit2ff58aa2c8592a5ce56815e10c8477f481ab25fd (patch)
tree38aeeb28a6ef5131fb65286b4dedc23d23cc54ac /contrib/extraction/ocaml.ml
parentc5d686f2abee4f7d6376cfbdbc2d49c42c423c17 (diff)
decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8724 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/ocaml.ml')
-rw-r--r--contrib/extraction/ocaml.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 088e66622..15d219e49 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -196,7 +196,7 @@ let rec pp_type par vl t =
| Tarr (t1,t2) ->
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
- | Tdummy -> str "__"
+ | Tdummy _ -> str "__"
| Tunknown -> str "__"
in
hov 0 (pp_rec par t)