diff options
author | Stephane Glondu <steph@glondu.net> | 2010-12-24 12:51:11 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 12:51:11 +0100 |
commit | 20d03a28285c430740d0b675583fe5c4d13ffecc (patch) | |
tree | 36bd87c5c42d948291605fc35b4b7cf573fc8113 /plugins/extraction/scheme.ml | |
parent | c0a92523eaa76afabcbaf06ac4a7e8f7930ee4a3 (diff) | |
parent | 50dc9067e98ca001ad2e875011abab5da6fdb621 (diff) |
Merge commit 'upstream/8.3.pl1+dfsg' into experimental/master
Diffstat (limited to 'plugins/extraction/scheme.ml')
-rw-r--r-- | plugins/extraction/scheme.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index fa293ba1..06098591 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: scheme.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) (*s Production of Scheme syntax. *) @@ -87,7 +87,7 @@ let rec pp_expr env args = ++ spc () ++ hov 0 (pp_expr env' [] a2))))) | MLglob r -> apply (pp_global Term r) - | MLcons (i,r,args') -> + | MLcons (info,r,args') -> assert (args=[]); let st = str "`" ++ @@ -95,7 +95,7 @@ let rec pp_expr env args = (if args' = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args') in - if i = Coinductive then paren (str "delay " ++ st) else st + if info.c_kind = Coinductive then paren (str "delay " ++ st) else st | MLcase (_,t,pv) when is_custom_match pv -> let mkfun (_,ids,e) = if ids <> [] then named_lams (List.rev ids) e @@ -104,9 +104,9 @@ let rec pp_expr env args = hov 2 (str (find_custom_match pv) ++ fnl () ++ prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv ++ pp_expr env [] t) - | MLcase ((i,_),t, pv) -> + | MLcase (info,t, pv) -> let e = - if i <> Coinductive then pp_expr env [] t + if info.m_kind <> Coinductive then pp_expr env [] t else paren (str "force" ++ spc () ++ pp_expr env [] t) in apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv))) @@ -123,7 +123,7 @@ let rec pp_expr env args = | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") and pp_cons_args env = function - | MLcons (i,r,args) when i<>Coinductive -> + | MLcons (info,r,args) when info.c_kind<>Coinductive -> paren (pp_global Cons r ++ (if args = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args) |