diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/extraction.ml | 1 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 10 |
2 files changed, 10 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index a1c88b7bd..72b949da6 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -400,6 +400,7 @@ and extract_term_with_type env ctx c t = | IsMutConstruct (cp,_) -> Rmlterm (MLglob (ConstructRef cp)) (* TODO eta-expansion *) | IsMutCase ((ni,(ip,cnames,_,_,_)),p,c,br) -> + (* TODO: [ni] probably without parameters *) let extract_branch j b = let (_,s) = extract_constructor (ip,succ j) in assert (List.length s = ni.(j)); diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index e990f5c0d..cae4a873e 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -262,7 +262,15 @@ let pp_decl = function | Dabbrev (id, l, t) -> hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; pr_id id; 'sPC; 'sTR "="; 'sPC; pp_type t >] + | Dglob (id, MLfix (n,_,idl,l)) -> + let id' = List.nth idl n in + if id = id' then + [< hOV 2 (pp_fix false [] (n,false,idl,l) []) >] + else + [< 'sTR "let "; pr_id id; 'sTR " ="; 'fNL; + v 0 [< 'sTR " "; + hOV 2 (pp_fix false [] (n,true,idl,l) []); 'fNL >] >] | Dglob (id, a) -> - hOV 0 [< 'sTR "let"; 'sPC; pr_id id; 'sPC; 'sTR "="; 'sPC; pp_ast a >] + hOV 0 [< 'sTR "let "; pp_function [] id a >] end |