to apply, e.g. H:(not A) to False.
let new_metasenv_for_apply newmeta proof context ty =
let module C = Cic in
let module S = CicSubstitution in
let new_metasenv_for_apply newmeta proof context ty =
let module C = Cic in
let module S = CicSubstitution in
- let rec aux newmeta =
- function
+ let rec aux newmeta ty =
+ let ty' = CicReduction.whd context ty in
+ match ty' with
C.Cast (he,_) -> aux newmeta he
(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
(* If the expected type is a Type, then also Set is OK ==>
C.Cast (he,_) -> aux newmeta he
(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
(* If the expected type is a Type, then also Set is OK ==>