X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_extraction%2FnCicExtraction.ml;h=8e384075cf20e8039704bcbfa3af5e0d8cfe60b5;hb=926bd86002f91d2bf2a3ce7376309f5106268959;hp=18b7086f513b93da9380c01996fca8d6c0dcd6de;hpb=66be8fbe19e2ccfa0e6a7abeba605152d1322595;p=helm.git diff --git a/matita/components/ng_extraction/nCicExtraction.ml b/matita/components/ng_extraction/nCicExtraction.ml index 18b7086f5..8e384075c 100644 --- a/matita/components/ng_extraction/nCicExtraction.ml +++ b/matita/components/ng_extraction/nCicExtraction.ml @@ -319,7 +319,7 @@ class virtual status = method extraction_db = extraction_db method set_extraction_db v = {< extraction_db = v >} method set_extraction_status - : 'status. #g_status as 'status -> 'self + : 'status. (#g_status as 'status) -> 'self = fun o -> {< extraction_db = o#extraction_db >} end @@ -1213,11 +1213,11 @@ let rec pp_obj status (_,ref,obj_kind) = | Algebraic il -> String.concat "\n" (List.map - (fun _,ref,left,right,cl -> + (fun (_,ref,left,right,cl) -> "data " ^ pp_ref status ref ^ " " ^ pretty_print_context (right@left) ^ " where\n " ^ String.concat "\n " (List.map - (fun ref,tys -> + (fun (ref,tys) -> let namectx = namectx_of_ctx left in pp_ref status ref ^ " :: " ^ pretty_print_type status namectx tys