Added a whd on ty in new_metasenv for apply, in order to be able

to apply, e.g. H:(not A) to False.

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 66a9c0930e934e21070e4a0bb0d85e762d5899d9..d7b910fcec94bc15619728c6baaf0c21352999dd 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -161,8 +161,9 @@ let classify_metas newmeta in_subst_domain subst_in metasenv =
 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 ==>