diff options
| author | letouzey | 2011-01-07 13:50:57 +0000 |
|---|---|---|
| committer | letouzey | 2011-01-07 13:50:57 +0000 |
| commit | 5056083eb0b6ad626fe24d9c85370e09c8c2db91 (patch) | |
| tree | 6796140d6a5f57d01773072323a9a11a1fc79127 /plugins/extraction/scheme.ml | |
| parent | 5db7b802bdf82f67b91fcf7371194400852595ea (diff) | |
Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13770 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/scheme.ml')
| -rw-r--r-- | plugins/extraction/scheme.ml | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 77c8e944e3..612da13499 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -161,15 +161,18 @@ let pp_decl = function | Dind _ -> mt () | Dtype _ -> mt () | Dfix (rv, defs,_) -> - let ppv = Array.map (pp_global Term) rv in - prvect_with_sep fnl - (fun (pi,ti) -> - hov 2 - (paren (str "define " ++ pi ++ spc () ++ - (pp_expr (empty_env ()) [] ti)) - ++ fnl ())) - (array_map2 (fun p b -> (p,b)) ppv defs) ++ - fnl () + let names = Array.map + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + in + prvecti + (fun i r -> + if is_inline_custom r then mt () + else + hov 2 + (paren (str "define " ++ names.(i) ++ spc () ++ + (pp_expr (empty_env ()) [] defs.(i))) + ++ fnl ()) ++ fnl ()) + rv | Dterm (r, a, _) -> if is_inline_custom r then mt () else |