diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-20 16:33:02 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-20 16:33:02 +0000 |
| commit | bfab127241c172a71e6f82158d7d3d72236cdc19 (patch) | |
| tree | 6a4faecff5d7d4c4dde8f4ee90e810466620bb81 | |
| parent | 578753fbd584d07968d694012f85f995ddaa0251 (diff) | |
affichage declarations fix + bug extraction sumbool_rec mis a jour
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1473 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |