+ (match bo with
+ None -> t
+ | Some bo ->
+ head_beta_reduce ~upto
+ ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
+ | Cic.Const (uri,ens) as t when delta=true ->
+ let bo =
+ match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+ Cic.Constant (_,bo,_,_,_) -> bo
+ | Cic.Variable _ -> raise ReferenceToVariable
+ | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+ | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ in
+ (match bo with
+ None -> t
+ | Some bo ->
+ head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo))
+ | t -> t
+
+(*
+let are_convertible ?subst ?metasenv context t1 t2 ugraph =
+ let before = Unix.gettimeofday () in
+ let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in
+ let after = Unix.gettimeofday () in
+ let diff = after -. before in
+ if diff > 0.1 then
+ begin
+ let nc = List.map (function None -> None | Some (n,_) -> Some n) context in
+ prerr_endline
+ ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc);
+ end;
+ res
+*)