aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/modutil.ml
diff options
context:
space:
mode:
authorletouzey2005-11-17 15:48:45 +0000
committerletouzey2005-11-17 15:48:45 +0000
commitf7e00f4bc292795bcef6b66c294a60cd4f61ccb0 (patch)
treee6e09387898683bf26c37373745f588196bfcff5 /contrib/extraction/modutil.ml
parent97a93cc747342931c37e205c60d8398bd45a2f28 (diff)
merci les warnings de 3.09 ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7574 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/modutil.ml')
-rw-r--r--contrib/extraction/modutil.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 673c8e929d..6dcfaf2a1f 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -185,7 +185,7 @@ let ast_iter_references do_term do_cons do_type a =
| MLcons (i,r,_) ->
if lang () = Ocaml then record_iter_references do_term i;
do_cons r
- | MLcase (i,_,v) as a ->
+ | MLcase (i,_,v) ->
if lang () = Ocaml then record_iter_references do_term i;
Array.iter (fun (r,_,_) -> do_cons r) v
| _ -> ()