diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-17 15:48:45 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-17 15:48:45 +0000 |
| commit | f7e00f4bc292795bcef6b66c294a60cd4f61ccb0 (patch) | |
| tree | e6e09387898683bf26c37373745f588196bfcff5 /contrib/extraction/ocaml.ml | |
| parent | 97a93cc747342931c37e205c60d8398bd45a2f28 (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/ocaml.ml')
| -rw-r--r-- | contrib/extraction/ocaml.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index f9b91d226..ee53bd49a 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -264,7 +264,6 @@ let rec pp_expr par env args = let tuple = pp_tuple (pp_expr true env []) args' in pp_par par (pp_global r ++ spc () ++ tuple) | MLcase (i, t, pv) -> - let r,_,_ = pv.(0) in let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else @@ -480,7 +479,7 @@ let pp_mind kn i = let pp_decl mpl = local_mpl := mpl; function - | Dind (kn,i) as d -> pp_mind kn i + | Dind (kn,i) -> pp_mind kn i | Dtype (r, l, t) -> if is_inline_custom r then failwith "empty phrase" else |