]> matita.cs.unibo.it Git - helm.git/commitdiff
Added a whd on ty in new_metasenv for apply, in order to be able
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 20 May 2005 15:24:18 +0000 (15:24 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 20 May 2005 15:24:18 +0000 (15:24 +0000)
to apply, e.g. H:(not A) to False.

helm/ocaml/tactics/primitiveTactics.ml

index 66a9c0930e934e21070e4a0bb0d85e762d5899d9..d7b910fcec94bc15619728c6baaf0c21352999dd 100644 (file)
@@ -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 ==>