with
WrongShape -> after_beta_expansion
-let unif_ty = ref true
-
let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
let module S = CicSubstitution in
let module C = Cic in
in
begin
let subst,metasenv,ugraph1 =
- if not (!unif_ty) then subst,metasenv,ugraph else
let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
(try
let tyt,ugraph1 =