From bfab127241c172a71e6f82158d7d3d72236cdc19 Mon Sep 17 00:00:00 2001 From: filliatr Date: Tue, 20 Mar 2001 16:33:02 +0000 Subject: 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 --- contrib/extraction/ocaml.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'contrib/extraction/ocaml.ml') 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 -- cgit v1.2.3