+ let ty_of_m _ = Cic.Implicit (Some `Type)
+(*
+ let ty_of_m = function
+ | Cic.Meta (i,_) ->
+ (try
+ let _,_,ty = CicUtil.lookup_meta i menv in ty
+ with CicUtil.Meta_not_found _ ->
+ prerr_endline "eccoci";assert false)
+ | _ -> assert false
+*)
+ (*