(CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
| (CicUnification.Uncertain msg) -> raise (Uncertain msg)
;;
+
+let enrich localization_tbl t ?(f = fun msg -> msg) exn =
+ let exn' =
+ match exn with
+ RefineFailure msg -> RefineFailure (f msg)
+ | Uncertain msg -> Uncertain (f msg)
+ | _ -> assert false in
+ let loc =
+ try
+ Cic.CicHash.find localization_tbl t
+ with Not_found ->
+ prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
+ assert false
+ in
+ raise (HExtlib.Localized (loc,exn'))
+
+let relocalize localization_tbl oldt newt =
+ try
+ let infos = Cic.CicHash.find localization_tbl oldt in
+ Cic.CicHash.remove localization_tbl oldt;
+ Cic.CicHash.add localization_tbl newt infos;
+ with
+ Not_found -> ()
+;;
let rec split l n =
match (l,n) with
| (_,_) -> raise (AssertFailure (lazy "split: list too short"))
;;
-let exp_impl metasenv subst context term =
- let rec aux metasenv context = function
- | (Cic.Rel _) as t -> metasenv, t
- | (Cic.Sort _) as t -> metasenv, t
- | Cic.Const (uri, subst) ->
- let metasenv', subst' = do_subst metasenv context subst in
- metasenv', Cic.Const (uri, subst')
- | Cic.Var (uri, subst) ->
- let metasenv', subst' = do_subst metasenv context subst in
- metasenv', Cic.Var (uri, subst')
- | Cic.MutInd (uri, i, subst) ->
- let metasenv', subst' = do_subst metasenv context subst in
- metasenv', Cic.MutInd (uri, i, subst')
- | Cic.MutConstruct (uri, i, j, subst) ->
- let metasenv', subst' = do_subst metasenv context subst in
- metasenv', Cic.MutConstruct (uri, i, j, subst')
- | Cic.Meta (n,l) ->
- let metasenv', l' = do_local_context metasenv context l in
- metasenv', Cic.Meta (n, l')
- | Cic.Implicit (Some `Type) ->
+let exp_impl metasenv subst context =
+ function
+ | Some `Type ->
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)
- | Cic.Implicit (Some `Closed) ->
+ | Some `Closed ->
let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
metasenv', Cic.Meta (idx, [])
- | Cic.Implicit None ->
+ | None ->
let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
metasenv', Cic.Meta (idx, irl)
- | Cic.Implicit _ -> assert false
- | Cic.Cast (te, ty) ->
- let metasenv', ty' = aux metasenv context ty in
- let metasenv'', te' = aux metasenv' context te in
- metasenv'', Cic.Cast (te', ty')
- | Cic.Prod (name, s, t) ->
- let metasenv', s' = aux metasenv context s in
- metasenv', Cic.Prod (name, s', t)
- | Cic.Lambda (name, s, t) ->
- let metasenv', s' = aux metasenv context s in
- metasenv', Cic.Lambda (name, s', t)
- | Cic.LetIn (name, s, t) ->
- let metasenv', s' = aux metasenv context s in
- metasenv', Cic.LetIn (name, s', t)
- | Cic.Appl l when List.length l > 1 ->
- let metasenv', l' =
- List.fold_right
- (fun term (metasenv, terms) ->
- let new_metasenv, term = aux metasenv context term in
- new_metasenv, term :: terms)
- l (metasenv, [])
- in
- metasenv', Cic.Appl l'
- | Cic.Appl _ -> assert false
- | Cic.MutCase (uri, i, outtype, term, patterns) ->
- let metasenv', l' =
- List.fold_right
- (fun term (metasenv, terms) ->
- let new_metasenv, term = aux metasenv context term in
- new_metasenv, term :: terms)
- (outtype :: term :: patterns) (metasenv, [])
- in
- let outtype', term', patterns' =
- match l' with
- | outtype' :: term' :: patterns' -> outtype', term', patterns'
- | _ -> assert false
- in
- metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
- | Cic.Fix (i, funs) ->
- let metasenv', types =
- List.fold_right
- (fun (name, _, typ, _) (metasenv, types) ->
- let new_metasenv, new_type = aux metasenv context typ in
- (new_metasenv, (name, new_type) :: types))
- funs (metasenv, [])
- in
- let rec combine = function
- | ((name, index, _, body) :: funs_tl),
- ((_, typ) :: typ_tl) ->
- (name, index, typ, body) :: combine (funs_tl, typ_tl)
- | [], [] -> []
- | _ -> assert false
- in
- let funs' = combine (funs, types) in
- metasenv', Cic.Fix (i, funs')
- | Cic.CoFix (i, funs) ->
- let metasenv', types =
- List.fold_right
- (fun (name, typ, _) (metasenv, types) ->
- let new_metasenv, new_type = aux metasenv context typ in
- (new_metasenv, (name, new_type) :: types))
- funs (metasenv, [])
- in
- let rec combine = function
- | ((name, _, body) :: funs_tl),
- ((_, typ) :: typ_tl) ->
- (name, typ, body) :: combine (funs_tl, typ_tl)
- | [], [] -> []
- | _ -> assert false
- in
- let funs' = combine (funs, types) in
- metasenv', Cic.CoFix (i, funs')
- and do_subst metasenv context subst =
- List.fold_right
- (fun (uri, term) (metasenv, substs) ->
- let metasenv', term' = aux metasenv context term in
- (metasenv', (uri, term') :: substs))
- subst (metasenv, [])
- and do_local_context metasenv context local_context =
- List.fold_right
- (fun term (metasenv, local_context) ->
- let metasenv', term' =
- match term with
- | None -> metasenv, None
- | Some term ->
- let metasenv', term' = aux metasenv context term in
- metasenv', Some term'
- in
- metasenv', term' :: local_context)
- local_context (metasenv, [])
- in
- aux metasenv context term
+ | _ -> assert false
;;
let rec type_of_constant uri ugraph =
| _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
| _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
-and type_of_aux' metasenv context t ugraph =
- let metasenv, t = exp_impl metasenv [] context t in
+and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
+ ugraph
+=
let rec type_of_aux subst metasenv context t ugraph =
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
- (* this stops on binders, so we have to call it every time *)
+ let (t',_,_,_,_) as res =
match t with
(* function *)
C.Rel n ->
(S.lift n bo) ugraph
in
t,ty,subst,metasenv,ugraph
- | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
+ | None ->
+ enrich localization_tbl t
+ (RefineFailure (lazy "Rel to hidden hypothesis"))
with
- _ -> raise (RefineFailure (lazy "Not a close term")))
+ _ ->
+ enrich localization_tbl t
+ (RefineFailure (lazy "Not a close term")))
| C.Var (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
check_exp_named_subst
t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
| C.Sort _ ->
t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
- | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+ | C.Implicit infos ->
+ let metasenv',t' = exp_impl metasenv subst context infos in
+ type_of_aux subst metasenv' context t' ugraph
| C.Cast (te,ty) ->
let ty',_,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context ty ugraph
let te',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv' context te ugraph1
in
- (try
- let subst''',metasenv''',ugraph3 =
- fo_unif_subst subst'' context metasenv''
- inferredty ty ugraph2
- in
- C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
- with
- | _ -> raise (RefineFailure (lazy "Cast")))
+ (try
+ let subst''',metasenv''',ugraph3 =
+ fo_unif_subst subst'' context metasenv''
+ inferredty ty' ugraph2
+ in
+ C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+ with
+ exn ->
+ enrich localization_tbl te'
+ ~f:(fun _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst'' te'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst'' inferredty
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
+ )
| C.Prod (name,s,t) ->
let carr t subst context = CicMetaSubst.apply_subst subst t in
- let coerce_to_sort
- in_source tgt_sort t type_to_coerce subst ctx metasenv uragph
+ let coerce_to_sort in_source tgt_sort t type_to_coerce
+ subst context metasenv uragph
=
- let coercion_src = carr type_to_coerce subst ctx in
+ let coercion_src = carr type_to_coerce subst context in
match coercion_src with
| Cic.Sort _ ->
t,type_to_coerce,subst,metasenv,ugraph
-(*
- | Cic.Meta _ as meta when not in_source ->
- let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
- let subst, metasenv, ugraph =
- fo_unif_subst
- subst ctx metasenv meta coercion_tgt ugraph
- in
- t, Cic.Sort tgt_sort, subst, metasenv, ugraph
-*)
| Cic.Meta _ as meta ->
t, meta, subst, metasenv, ugraph
| Cic.Cast _ as cast ->
t, cast, subst, metasenv, ugraph
| term ->
- let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
+ let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
let search = CoercGraph.look_for_coercion in
let boh = search coercion_src coercion_tgt in
(match boh with
- | CoercGraph.NoCoercion ->
- raise (RefineFailure (lazy "no coercion"))
- | CoercGraph.NotHandled _ ->
- raise (RefineFailure (lazy "not a sort in PI"))
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
+ enrich localization_tbl t
+ (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
| CoercGraph.NotMetaClosed ->
- raise (Uncertain (lazy "Coercions on metas 1"))
+ enrich localization_tbl t
+ (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
| CoercGraph.SomeCoercion c ->
Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
in
s' sort1 subst' context metasenv' ugraph1
in
let context_for_t = ((Some (name,(C.Decl s')))::context) in
- let metasenv',t = exp_impl metasenv' subst' context_for_t t in
let t',sort2,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv'
context_for_t t ugraph1
| C.Lambda (n,s,t) ->
let s',sort1,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- (match CicReduction.whd ~subst:subst' context sort1 with
+ type_of_aux subst metasenv context s ugraph in
+ let s',sort1 =
+ match CicReduction.whd ~subst:subst' context sort1 with
C.Meta _
- | C.Sort _ -> ()
- | _ ->
- raise (RefineFailure (lazy (sprintf
- "Not well-typed lambda-abstraction: the source %s should be a type;
- instead it is a term of type %s" (CicPp.ppterm s)
- (CicPp.ppterm sort1))))
- ) ;
+ | C.Sort _ -> s',sort1
+ | coercion_src ->
+ let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in
+ let search = CoercGraph.look_for_coercion in
+ let boh = search coercion_src coercion_tgt in
+ match boh with
+ | CoercGraph.SomeCoercion c ->
+ Cic.Appl [c;s'], coercion_tgt
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
+ enrich localization_tbl s'
+ (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.NotMetaClosed ->
+ enrich localization_tbl s'
+ (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
+ in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
- let metasenv',t = exp_impl metasenv' subst' context_for_t t in
let t',type2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv'
- context_for_t t ugraph1
+ type_of_aux subst' metasenv' context_for_t t ugraph1
in
C.Lambda (n,s',t'),C.Prod (n,s',type2),
subst'',metasenv'',ugraph2
type_of_aux subst metasenv context s ugraph
in
let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
- let metasenv',t = exp_impl metasenv' subst' context_for_t t in
let t',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv'
let x',ty,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context x ugraph
in
- (x', ty)::res,subst',metasenv',ugraph1
+ (x', ty)::res,subst',metasenv',ugraph1
) tl ([],subst',metasenv',ugraph1)
in
let tl',applty,subst''',metasenv''',ugraph3 =
- eat_prods subst'' metasenv'' context
+ eat_prods true subst'' metasenv'' context
hetype tlbody_and_type ugraph2
in
C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
- | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
+ | C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
check_exp_named_subst subst metasenv context
C.InductiveDefinition (l,expl_params,parsno,_) ->
List.nth l i , expl_params, parsno, u
| _ ->
- raise
- (RefineFailure
- (lazy ("Unkown mutual inductive definition " ^
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy ("Unkown mutual inductive definition " ^
U.string_of_uri uri)))
in
let rec count_prod t =
in
let actual_type = CicReduction.whd ~subst context actual_type in
let subst,metasenv,ugraph3 =
+ try
fo_unif_subst subst context metasenv
expected_type' actual_type ugraph2
+ with
+ exn ->
+ enrich localization_tbl term' exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst term'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst actual_type
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst expected_type' context))
in
let rec instantiate_prod t =
function
its instances
*)
+ let outtype,outtypety, subst, metasenv,ugraph4 =
+ type_of_aux subst metasenv context outtype ugraph4 in
(match outtype with
| C.Meta (n,l) ->
(let candidate,ugraph5,metasenv,subst =
(Cic.Appl (outtype::right_args@[term']))),
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)
+ in
+ let _,_,subst,metasenv,ugraph4 =
+ eat_prods false subst metasenv context
+ outtypety tlbody_and_type ugraph4
+ in
let _,_, subst, metasenv,ugraph5 =
type_of_aux subst metasenv context
(C.Appl ((outtype :: right_args) @ [term'])) ugraph4
let fl_bo',subst,metasenv,ugraph2 =
List.fold_left
(fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
- let metasenv, bo = exp_impl metasenv subst context' bo in
let bo',ty_of_bo,subst,metasenv,ugraph1 =
type_of_aux subst metasenv context' bo ugraph
in
let fl_bo',subst,metasenv,ugraph2 =
List.fold_left
(fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
- let metasenv, bo = exp_impl metasenv subst context' bo in
let bo',ty_of_bo,subst,metasenv,ugraph1 =
type_of_aux subst metasenv context' bo ugraph
in
fl_ty' fl_bo' fl
in
C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
+ in
+ relocalize localization_tbl t t';
+ res
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
match tl with
[] -> [],metasubst,metasenv,ugraph
- | ((uri,t) as subst)::tl ->
+ | (uri,t)::tl ->
let ty_uri,ugraph1 = type_of_variable uri ugraph in
let typeofvar =
CicSubstitution.subst_vars substs ty_uri in
) ;
*)
let t',typeoft,metasubst',metasenv',ugraph2 =
- type_of_aux metasubst metasenv context t ugraph1
- in
+ type_of_aux metasubst metasenv context t ugraph1 in
+ let subst = uri,t' in
let metasubst'',metasenv'',ugraph3 =
try
fo_unif_subst
(CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
(CicPp.ppterm t2''))))
- and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
+ and eat_prods
+ allow_coercions subst metasenv context hetype tlbody_and_type ugraph
+ =
let rec mk_prod metasenv context =
function
[] ->
fo_unif_subst subst context metasenv hety s ugraph
in
hete,subst,metasenv,ugraph1
- with exn ->
+ with exn when allow_coercions ->
(* we search a coercion from hety to s *)
let coer =
let carr t subst context =
in
match coer with
| CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ -> raise exn
+ | 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 ->
- raise (Uncertain (lazy "Coercions on meta"))
+ 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 c ->
(Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
in
let coerced_args,metasenv',subst',t',ugraph2 =
eat_prods metasenv subst context
- (* (CicMetaSubst.subst subst hete t) tl *)
- (CicSubstitution.subst hete t) ugraph1 tl
+ (CicSubstitution.subst arg t) ugraph1 tl
in
arg::coerced_args,metasenv',subst',t',ugraph2
| _ -> assert false
(cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
;;
-let type_of_aux' metasenv context term ugraph =
+let type_of_aux' ?localization_tbl metasenv context term ugraph =
try
- type_of_aux' metasenv context term ugraph
+ type_of_aux' ?localization_tbl metasenv context term ugraph
with
CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
(*CSC: this is a very rough approximation; to be finished *)
let are_all_occurrences_positive metasenv ugraph uri tys leftno =
- let number_of_types = List.length tys in
let subst,metasenv,ugraph,tys =
List.fold_right
(fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
in
metasenv,ugraph,substituted_tys
-let typecheck metasenv uri obj =
+let typecheck metasenv uri obj ~localization_tbl =
let ugraph = CicUniv.empty_ugraph in
match obj with
Cic.Constant (name,Some bo,ty,args,attrs) ->
- let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
- let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ let bo',boty,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] bo ugraph in
+ let ty',_,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] ty ugraph in
let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
let bo' = CicMetaSubst.apply_subst subst bo' in
let ty' = CicMetaSubst.apply_subst subst ty' in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
| Cic.Constant (name,None,ty,args,attrs) ->
- let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ let ty',_,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] ty ugraph
+ in
Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
| Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
assert (metasenv' = metasenv);
(* Here we do not check the metasenv for correctness *)
- let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
- let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ let bo',boty,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] bo ugraph in
+ let ty',sort,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] ty ugraph in
begin
match sort with
Cic.Sort _
let metasenv,ugraph,tys =
List.fold_right
(fun (name,b,ty,cl) (metasenv,ugraph,res) ->
- let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ let ty',_,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] ty ugraph
+ in
metasenv,ugraph,(name,b,ty',cl)::res
) tys (metasenv,ugraph,[]) in
let con_context =
(fun (name,ty) (metasenv,ugraph,res) ->
let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
let ty',_,metasenv,ugraph =
- type_of_aux' metasenv con_context ty ugraph in
+ type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
let ty' = undebrujin uri typesno tys ty' in
metasenv,ugraph,(name,ty')::res
) cl (metasenv,ugraph,[])
let profiler2 = HExtlib.profile "CicRefine"
-let type_of_aux' metasenv context term ugraph =
- profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
+let type_of_aux' ?localization_tbl metasenv context term ugraph =
+ profiler2.HExtlib.profile
+ (type_of_aux' ?localization_tbl metasenv context term) ugraph
-let typecheck metasenv uri obj =
- profiler2.HExtlib.profile (typecheck metasenv uri) obj
+let typecheck ~localization_tbl metasenv uri obj =
+ profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
projects / helm.git / blobdiff