From c5dbc685d2ef5c3b929efefda75478c59eac6fef Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 20 May 2005 15:24:18 +0000 Subject: [PATCH] Added a whd on ty in new_metasenv for apply, in order to be able to apply, e.g. H:(not A) to False. --- helm/ocaml/tactics/primitiveTactics.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 ==> -- 2.39.2