(* we search a coercion from hety to s *)
let coer, tgt_carr =
let carr t subst context =
- CicMetaSubst.apply_subst subst t
+ 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
| C.LetIn (name,so,dest) ->
let ctx' = Some (name,(C.Def (so,None)))::ctx in
C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.Appl l as 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
(* prerr_endline "CANDIDATO!!!!"; *)
- let newt =
- if b then
- let ugraph = CicUniv.empty_ugraph in
- let old_insert_coercions = !insert_coercions in
- insert_coercions := false;
- let newt, _, menv, _ =
- try
- type_of_aux' metasenv ctx t ugraph
- with RefineFailure _ | Uncertain _ ->
- prerr_endline (CicPp.ppterm t);
- t, t, [], ugraph
- in
- insert_coercions := old_insert_coercions;
- if metasenv <> [] || menv = [] then
- newt
- else
- (prerr_endline "PUO' SUCCEDERE!!!!!";t)
- else
- t
- in
- (match newt with
- | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
- | _ -> assert false)
+ if b then
+ let ugraph = CicUniv.empty_ugraph in
+ let old_insert_coercions = !insert_coercions in
+ insert_coercions := false;
+ let newt, _, menv, _ =
+ try
+ type_of_aux' metasenv ctx t ugraph
+ with RefineFailure _ | Uncertain _ ->
+ prerr_endline (CicPp.ppterm t);
+ t, t, [], ugraph
+ in
+ insert_coercions := old_insert_coercions;
+ if metasenv <> [] || menv = [] then
+ newt
+ else
+ (prerr_endline "PUO' SUCCEDERE!!!!!";t)
+ else
+ t
| C.Var (uri,exp_named_subst) ->
let exp_named_subst = List.map aux exp_named_subst in
C.Var (uri, exp_named_subst)
let typecheck ~localization_tbl metasenv uri obj =
profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
+
+let _ = DoubleTypeInference.pack_coercion := pack_coercion;;