X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=798c38540d5118cc4f3f8ab190152d1dcfdebdd4;hb=2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8;hp=48ae522f4c9b4b170111a2dabff110e93388d863;hpb=f764844fa35ab0bb9c10707151340b924060f069;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 48ae522f4..798c38540 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -32,8 +32,10 @@ exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; let insert_coercions = ref true +let pack_coercions = ref true let debug_print = fun _ -> () +(* let debug_print x = prerr_endline (Lazy.force x);; *) let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2" @@ -123,24 +125,76 @@ let exp_impl metasenv subst context = let is_a_double_coercion t = let last_of l = - let rec aux = function - | x::[] -> x - | x::tl -> aux tl + let rec aux acc = function + | x::[] -> acc,x + | x::tl -> aux (acc@[x]) tl | [] -> assert false in - aux l - in - let dummyres = - false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None + aux [] l in + let imp = Cic.Implicit None in + let dummyres = false,imp, imp,imp,imp in match t with | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 -> (match last_of tl with - | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> - let head = last_of tl2 in - true, c1, c2, head + | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> + let sib2,head = last_of tl2 in + true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl + (c2::sib2@[Cic.Implicit None])]) | _ -> dummyres) | _ -> dummyres + +let more_args_than_expected subst he context hetype' tlbody_and_type = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst he context ^ + " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype' context ^ + ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ + " arguments that are more than expected") +;; + +let mk_prod_of_metas metasenv context' subst args = + let rec mk_prod metasenv context' = function + | [] -> + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context' + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context' + in + metasenv,Cic.Meta (idx, irl) + | (_,argty)::tl -> + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context' + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context' + in + let meta = Cic.Meta (idx,irl) in + let name = + (* The name must be fresh for context. *) + (* Nevertheless, argty is well-typed only in context. *) + (* Thus I generate a name (name_hint) in context and *) + (* then I generate a name --- using the hint name_hint *) + (* --- that is fresh in context'. *) + let name_hint = + (* Cic.Name "pippo" *) + FreshNamesGenerator.mk_fresh_name ~subst metasenv + (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) + (CicMetaSubst.apply_subst_context subst context') + Cic.Anonymous + ~typ:(CicMetaSubst.apply_subst subst argty) + in + (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) + FreshNamesGenerator.mk_fresh_name ~subst + [] context' name_hint ~typ:(Cic.Sort Cic.Prop) + in + let metasenv,target = + mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl + in + metasenv,Cic.Prod (name,meta,target) + in + mk_prod metasenv context' args +;; let rec type_of_constant uri ugraph = let module C = Cic in @@ -526,20 +580,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t type_of_aux subst metasenv context he ugraph in let tlbody_and_type,subst'',metasenv'',ugraph2 = - List.fold_right - (fun x (res,subst,metasenv,ugraph) -> - let x',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context x ugraph - in - (x', ty)::res,subst',metasenv',ugraph1 - ) tl ([],subst',metasenv',ugraph1) + typeof_list subst' metasenv' context ugraph1 tl in - let tl',applty,subst''',metasenv''',ugraph3 = + let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 = eat_prods true subst'' metasenv'' context he' hetype tlbody_and_type ugraph2 in - avoid_double_coercion context - subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty + let newappl = (C.Appl (coerced_he::coerced_args)) in + avoid_double_coercion + context subst''' metasenv''' ugraph3 newappl applty | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = @@ -816,15 +865,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t subst,metasenv,ugraph) | _ -> (* easy case *) let tlbody_and_type,subst,metasenv,ugraph4 = - List.fold_right - (fun x (res,subst,metasenv,ugraph) -> - let x',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context x ugraph - in - (x', ty)::res,subst',metasenv',ugraph1 - ) (right_args @ [term']) ([],subst,metasenv,ugraph4) + typeof_list subst metasenv context ugraph4 (right_args @ [term']) in - let _,_,subst,metasenv,ugraph4 = + let _,_,_,subst,metasenv,ugraph4 = eat_prods false subst metasenv context outtype outtypety tlbody_and_type ugraph4 in @@ -1126,7 +1169,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (CicPp.ppterm t2'')))) and avoid_double_coercion context subst metasenv ugraph t ty = - let b, c1, c2, head = is_a_double_coercion t in + let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in if b then let source_carr = CoercGraph.source_of c2 in let tgt_carr = CicMetaSubst.apply_subst subst ty in @@ -1135,207 +1178,326 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (fun c -> + (function + | c when not (CoercGraph.is_composite c) -> + debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); + None + | c -> let newt = match c with | Cic.Appl l -> Cic.Appl (l @ [head]) | _ -> Cic.Appl [c;head] in + debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt)); (try - let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context newt ugraph in - let subst, metasenv, ugraph = - fo_unif_subst subst context metasenv newt t ugraph - in debug_print (lazy ("packing: " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); + let newt,_,subst,metasenv,ugraph = + type_of_aux subst metasenv context newt ugraph in + debug_print (lazy "tipa..."); + let subst, metasenv, ugraph = + (* COME MAI C'ERA UN IF su !pack_coercions ??? *) + fo_unif_subst subst context metasenv newt t ugraph + in + debug_print (lazy "unifica..."); Some (newt, ty, subst, metasenv, ugraph) - with RefineFailure _ | Uncertain _ -> None)) + with + | RefineFailure s | Uncertain s when not !pack_coercions-> + debug_print s; debug_print (lazy "stop\n");None + | RefineFailure s | Uncertain s -> + debug_print s;debug_print (lazy "goon\n"); + try + pack_coercions := false; (* to avoid diverging *) + let refined_c1_c2_implicit,ty,subst,metasenv,ugraph = + type_of_aux subst metasenv context c1_c2_implicit ugraph + in + pack_coercions := true; + let b, _, _, _, _ = + is_a_double_coercion refined_c1_c2_implicit + in + if b then + None + else + let head' = + match refined_c1_c2_implicit with + | Cic.Appl l -> HExtlib.list_last l + | _ -> assert false + in + let subst, metasenv, ugraph = + try fo_unif_subst subst context metasenv + head head' ugraph + with RefineFailure s| Uncertain s-> + debug_print s;assert false + in + let subst, metasenv, ugraph = + fo_unif_subst subst context metasenv + refined_c1_c2_implicit t ugraph + in + Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph) + with + | RefineFailure s | Uncertain s -> + pack_coercions := true;debug_print s;None + | exn -> pack_coercions := true; raise exn)) candidates in (match selected with | Some x -> x | None -> - prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t); - assert false) + debug_print + (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t)); + t, ty, subst, metasenv, ugraph) | _ -> assert false) (* the composite coercion must exist *) else t, ty, subst, metasenv, ugraph + and typeof_list subst metasenv context ugraph l = + let tlbody_and_type,subst,metasenv,ugraph = + List.fold_right + (fun x (res,subst,metasenv,ugraph) -> + let x',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context x ugraph + in + (x', ty)::res,subst',metasenv',ugraph1 + ) l ([],subst,metasenv,ugraph) + in + tlbody_and_type,subst,metasenv,ugraph + and eat_prods - allow_coercions subst metasenv context he hetype tlbody_and_type ugraph + allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph = - let rec mk_prod metasenv context' = - function - [] -> - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context' - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' - in - metasenv,Cic.Meta (idx, irl) - | (_,argty)::tl -> - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context' - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' - in - let meta = Cic.Meta (idx,irl) in - let name = - (* The name must be fresh for context. *) - (* Nevertheless, argty is well-typed only in context. *) - (* Thus I generate a name (name_hint) in context and *) - (* then I generate a name --- using the hint name_hint *) - (* --- that is fresh in context'. *) - let name_hint = - (* Cic.Name "pippo" *) - FreshNamesGenerator.mk_fresh_name ~subst metasenv - (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) - (CicMetaSubst.apply_subst_context subst context) - Cic.Anonymous - ~typ:(CicMetaSubst.apply_subst subst argty) - in - (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) - FreshNamesGenerator.mk_fresh_name ~subst - [] context' name_hint ~typ:(Cic.Sort Cic.Prop) - in - let metasenv,target = - mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl - in - metasenv,Cic.Prod (name,meta,target) - in - let ((subst,metasenv,ugraph1),hetype') = - if CicUtil.is_meta_closed hetype then - (subst,metasenv,ugraph),hetype - else - let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in - try - fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype' - with exn -> - enrich localization_tbl he - ~f:(fun _ -> - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst he - context ^ " (that has type " ^ - CicMetaSubst.ppterm_in_context subst hetype - context ^ ") is here applied to " ^ - string_of_int (List.length tlbody_and_type) ^ - " arguments that are more than expected" - (* "\nReason: " ^ Lazy.force exn*)))) exn + (* aux function to add coercions to funclass *) + let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph = + (* {{{ body *) + let pristinemenv = metasenv in + let metasenv,hetype' = + mk_prod_of_metas metasenv context subst args_bo_and_ty + in + try + let subst,metasenv,ugraph = + fo_unif_subst_eat_prods + subst context metasenv hetype hetype' ugraph + in + subst,metasenv,ugraph,hetype',he,args_bo_and_ty + with RefineFailure s | Uncertain s as exn + when allow_coercions && !insert_coercions -> + (* {{{ we search a coercion of the head (saturated) to funclass *) + let metasenv = pristinemenv in + debug_print (lazy + ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^ + " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' ^ + " cause: " ^ Lazy.force s)); + let how_many_args_are_needed = + let rec aux n = function + | Cic.Prod(_,_,t) -> aux (n+1) t + | _ -> n + in + aux 0 (CicMetaSubst.apply_subst subst hetype) + in + let args, remainder = + HExtlib.split_nth how_many_args_are_needed args_bo_and_ty + in + let args = List.map fst args in + let x = + if args <> [] then + match he with + | Cic.Appl l -> Cic.Appl (l@args) + | _ -> Cic.Appl (he::args) + else + he + in + let x,xty,subst,metasenv,ugraph = + type_of_aux subst metasenv context x ugraph + in + let carr_src = + CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) + in + let carr_tgt = CoercDb.Fun 0 in + match CoercGraph.look_for_coercion' carr_src carr_tgt with + | CoercGraph.NoCoercion + | CoercGraph.NotMetaClosed + | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.SomeCoercion candidates -> + match + HExtlib.list_findopt + (fun coerc -> + let t = Cic.Appl [coerc;x] in + debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t)); + try + (* we want this to be available in the error handler fo the + * following (so it has its own try. *) + let t,tty,subst,metasenv,ugraph = + type_of_aux subst metasenv context t ugraph + in + try + let metasenv, hetype' = + mk_prod_of_metas metasenv context subst remainder + in + debug_print (lazy + (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^ + CicMetaSubst.ppterm subst hetype')); + let subst,metasenv,ugraph = + fo_unif_subst_eat_prods + subst context metasenv tty hetype' ugraph + in + debug_print (lazy " success!"); + Some (subst,metasenv,ugraph,tty,t,remainder) + with + | Uncertain _ | RefineFailure _ + | CicUnification.UnificationFailure _ + | CicUnification.Uncertain _ -> + try + let subst,metasenv,ugraph,hetype',he,args_bo_and_ty = + fix_arity + metasenv context subst t tty remainder ugraph + in + Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) + with exn -> None + with exn -> None) + candidates + with + | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> + subst,metasenv,ugraph,hetype',he,args_bo_and_ty + | None -> + enrich localization_tbl he + ~f:(fun _-> more_args_than_expected subst he context hetype + args_bo_and_ty) exn + (* }}} end coercion to funclass stuff *) + (* }}} end fix_arity *) in - let rec eat_prods metasenv subst context hetype ugraph = + (* aux function to process the type of the head and the args in parallel *) + let rec eat_prods_and_args + pristinemenv metasenv subst context he hetype ugraph newargs + = + (* {{{ body *) function - | [] -> [],metasenv,subst,hetype,ugraph + | [] -> newargs,subst,metasenv,he,hetype,ugraph | (hete, hety)::tl -> - (match (CicReduction.whd ~subst context hetype) with - Cic.Prod (n,s,t) -> - let arg,subst,metasenv,ugraph1 = - try - let subst,metasenv,ugraph1 = - fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph - in - hete,subst,metasenv,ugraph1 - with exn when allow_coercions && !insert_coercions -> - (* we search a coercion from hety to s *) - let coer, tgt_carr = - let carr t subst context = - CicReduction.whd ~delta:false - context (CicMetaSubst.apply_subst subst t ) - in - let c_hety = carr hety subst context in - let c_s = carr s subst context in - CoercGraph.look_for_coercion c_hety c_s, c_s - in - (match coer with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - enrich localization_tbl hete - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl hete - (Uncertain - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.SomeCoercion candidates -> - let selected = - HExtlib.list_findopt - (fun c -> - try - let t = Cic.Appl[c;hete] in - let newt,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context - t ugraph - in - let newt, _, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv - ugraph newt tgt_carr - in - let subst,metasenv,ugraph1 = - fo_unif_subst subst context metasenv - newhety s ugraph - in - Some (newt, subst, metasenv, ugraph) - with Uncertain _ | RefineFailure _ -> None) - candidates - in - (match selected with - | Some x -> x - | None -> - enrich localization_tbl hete - ~f:(fun _ -> - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) exn)) - | exn -> + match (CicReduction.whd ~subst context hetype) with + | Cic.Prod (n,s,t) -> + let arg,subst,metasenv,ugraph1 = + try + let subst,metasenv,ugraph1 = + fo_unif_subst_eat_prods2 + subst context metasenv hety s ugraph + in + (hete,hety),subst,metasenv,ugraph1 + (* {{{ we search a coercion from hety to s if fails *) + with RefineFailure _ | Uncertain _ as exn + when allow_coercions && !insert_coercions -> + let coer, tgt_carr = + let carr t subst context = + CicReduction.whd ~delta:false + context (CicMetaSubst.apply_subst subst t ) + in + let c_hety = carr hety subst context in + let c_s = carr s subst context in + CoercGraph.look_for_coercion c_hety c_s, c_s + in + (match coer with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> enrich localization_tbl hete - ~f:(fun _ -> + (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context subst hety context ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) exn - in - let coerced_args,metasenv',subst',t',ugraph2 = - eat_prods metasenv subst context - (CicSubstitution.subst arg t) ugraph1 tl - in - arg::coerced_args,metasenv',subst',t',ugraph2 - | _ -> - raise (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst he - context ^ " (that has type " ^ - CicMetaSubst.ppterm_in_context subst hetype' - context ^ ") is here applied to " ^ - string_of_int (List.length tlbody_and_type) ^ - " arguments that are more than expected")))) + (* "\nReason: " ^ Lazy.force e*)))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl hete + (Uncertain + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (fun c -> + try + let t = Cic.Appl[c;hete] in + let newt,newhety,subst,metasenv,ugraph = + type_of_aux subst metasenv context + t ugraph + in + let newt, newty, subst, metasenv, ugraph = + avoid_double_coercion context subst metasenv + ugraph newt tgt_carr + in + let subst,metasenv,ugraph1 = + fo_unif_subst subst context metasenv + newhety s ugraph + in + Some ((newt,newty), subst, metasenv, ugraph) + with Uncertain _ | RefineFailure _ -> None) + candidates + in + (match selected with + | Some x -> x + | None -> + enrich localization_tbl hete + ~f:(fun _ -> + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) exn)) + | exn -> + enrich localization_tbl hete + ~f:(fun _ -> + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context ^ + "\nReason: " ^ Printexc.to_string exn))) exn + (* }}} end coercion stuff *) + in + eat_prods_and_args pristinemenv metasenv subst context he + (CicSubstitution.subst (fst arg) t) + ugraph1 (newargs@[arg]) tl + | _ -> + try + let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = + fix_arity + pristinemenv context subst he hetype + (newargs@[hete,hety]@tl) ugraph + in + eat_prods_and_args metasenv + metasenv subst context he hetype' ugraph [] args_bo_and_ty + with RefineFailure s | Uncertain s -> + (* unable to fix arity *) + let msg = + more_args_than_expected + subst he context hetype args_bo_and_ty + in + raise (RefineFailure msg) + (* }}} *) + in + (* first we check if we are in the simple case of a meta closed term *) + let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = + if CicUtil.is_meta_closed hetype then + (* this optimization is to postpone fix_arity (the most common case)*) + subst,metasenv,ugraph,hetype,he,args_bo_and_ty + else + (* this (says CSC) is also useful to infer dependent types *) + fix_arity metasenv context subst he hetype args_bo_and_ty ugraph in - let coerced_args,metasenv,subst,t,ugraph2 = - eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type + let coerced_args,subst,metasenv,he,t,ugraph = + eat_prods_and_args + metasenv metasenv subst context he hetype' ugraph1 [] args_bo_and_ty in - coerced_args,t,subst,metasenv,ugraph2 + he,(List.map fst coerced_args),t,subst,metasenv,ugraph in (* eat prods ends here! *) @@ -1566,7 +1728,7 @@ let pack_coercion metasenv ctx t = | C.Appl l -> let l = List.map (merge_coercions ctx) l in let t = C.Appl l in - let b,_,_,_ = is_a_double_coercion t in + let b,_,_,_,_ = is_a_double_coercion t in (* prerr_endline "CANDIDATO!!!!"; *) if b then let ugraph = CicUniv.empty_ugraph in @@ -1721,3 +1883,4 @@ let typecheck ~localization_tbl metasenv uri obj = profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj let _ = DoubleTypeInference.pack_coercion := pack_coercion;; +(* vim:set foldmethod=marker: *)