From: Stefano Zacchiroli Date: Wed, 24 Mar 2004 16:52:15 +0000 (+0000) Subject: CSC: hack to make applications of constants that have a Type sort which X-Git-Tag: dead_dir_walking~110 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=62792f5bfe558e6ba0e52e4e51841f4bc02a960a;p=helm.git CSC: hack to make applications of constants that have a Type sort which occurs in contravariant position work. The idea is to generate in place of a metavariable of type Type (that should be of type aux newmeta he + (* If the expected type is a Type, then also Set is OK ==> + * we accept any term of type Type *) + (*CSC: BUG HERE: in this way it is possible for the term of + * type Type to be different from a Sort!!! *) + | C.Prod (name,(C.Sort C.Type as s),t) -> + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let newargument = C.Meta (newmeta+1,irl) in + let (res,newmetasenv,arguments,lastmeta) = + aux (newmeta + 2) (S.subst newargument t) + in + res, + (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv, + newargument::arguments,lastmeta | C.Prod (name,s,t) -> let irl = CicMkImplicit.identity_relocation_list_for_metavariable context @@ -275,7 +290,7 @@ let apply_tac ~term ~status:(proof, goal) = in let newmetasenv = metasenv'@newmetas in let subst,newmetasenv' = - CicUnification.fo_unif newmetasenv context consthead ty + CicUnification.fo_unif newmetasenv context consthead ty in let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in let apply_subst = CicMetaSubst.apply_subst subst in