+ | exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
+ CicRefine.pack_coercions := old_pack_coercions;
+ raise exn
+ in
+ let c_ty, univ =
+ CicTypeChecker.type_of_aux' ~subst:[] [] [] c univ
+ in
+ let real_composed = ref true in
+ let c =
+ let rec is_id = function
+ | Cic.Lambda(_,_,t) -> is_id t
+ | Cic.Rel 1 -> true
+ | _ -> false
+ in
+ let is_id = function
+ | Cic.Const (u,_) ->
+ (match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+ | Cic.Constant (_,Some bo,_,_,_), _ -> is_id bo
+ | _ -> false)
+ | _ -> false
+ in
+ let unvariant u =
+ match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+ | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+ when List.exists ((=) (`Flavour `Variant)) attrs ->
+ u'
+ | _ -> u
+ in
+ let is_variant u =
+ match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+ | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+ when List.exists ((=) (`Flavour `Variant)) attrs -> true
+ | _ -> false
+ in
+ let rec aux = function
+ | Cic.Lambda(n,s,t) -> Cic.Lambda(n,s,aux t)
+ | Cic.Appl (c::_) as t ->
+ let t =
+ if is_id c then
+ (real_composed := false ;
+ CicReduction.head_beta_reduce ~delta:true t)
+ else t
+ in
+ (match t with
+ | Cic.Appl l -> Cic.Appl (List.map aux l)
+ | Cic.Const (u,[]) when is_variant u -> Cic.Const (unvariant u,[])
+ | t -> t)
+ | Cic.Const (u,[]) when is_variant u -> Cic.Const (unvariant u,[])
+ | t -> t
+ in
+ let simple_eta_c t =
+ let incr =
+ List.map (function Cic.Rel n -> Cic.Rel (n+1) | _ -> assert false)
+ in
+ let rec aux acc ctx = function
+ | Cic.Lambda (n,s,tgt) ->
+ aux (incr acc @ [Cic.Rel 1]) (Some (n,Cic.Decl s) ::ctx) tgt
+ | Cic.Appl (t::tl) when tl = acc &&
+ CicTypeChecker.does_not_occur ctx 0 (List.length acc) t -> true, t
+ | t -> false, t
+ in
+ let b, newt = aux [] [] t in
+ if b then newt else t
+ in
+ simple_eta_c (aux c)
+ in
+ debug_print (lazy ("COMPOSED COMPRESSED: " ^ string_of_bool !real_composed ^" : " ^ CicPp.ppterm c));
+ c, c_ty, metasenv, univ, saturationsres, arity2, cpos, !real_composed