From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 May 2005 15:24:18 +0000 (+0000)
Subject: Added a whd on ty in new_metasenv for apply, in order to be able
X-Git-Tag: single_binding~30
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c5dbc685d2ef5c3b929efefda75478c59eac6fef;p=helm.git

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 66a9c0930..d7b910fce 100644
--- 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 ==>