X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=d73b4fddb5345db76a5663bf717a63bff111ba47;hb=e085135177f7b3b74b410d47a4f3bca1784b60b1;hp=7871d86e92052728a1828627783c0c83642fec24;hpb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 7871d86e9..d73b4fddb 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -263,6 +263,22 @@ let rec typeof hdb in let metasenv, subst, outtype, outsort = typeof_aux metasenv subst context None outtype in + + (* next lines are to do a subst-expansion of the outtype, so + that when it becomes a beta-abstraction, the beta-redex is + fired during substitution *) + (*CSC: this is instantiate! should we move it from tactics to the + refiner? I think so! *) + let metasenv,metanoouttype,newouttype,metaoutsort = + NCicMetaSubst.mk_meta metasenv context `Term in + let metasenv,subst = + NCicUnification.unify hdb metasenv subst context outsort metaoutsort in + let metasenv = + List.filter (function (j,_) -> j <> metanoouttype) metasenv in + let subst = + (metanoouttype,(Some "outtype",context,outtype,metaoutsort))::subst in + let outtype = newouttype in + (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) let ind = if parameters = [] then C.Const r @@ -309,7 +325,7 @@ let rec typeof hdb let resty = C.Appl (outtype::arguments@[term]) in let resty = NCicReduction.head_beta_reduce ~subst resty in metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty - | C.Match _ as orig -> assert false + | C.Match _ -> assert false in pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^ NCicPp.ppterm ~metasenv ~subst ~context infty )); @@ -586,7 +602,7 @@ let typeof_obj hdb uri, height, metasenv, subst, C.Fixpoint (inductive, fl, attr) - | C.Inductive (ind, leftno, itl, attr) -> assert false + | C.Inductive (_ind, _leftno, _itl, _attr) -> assert false (* (* let's check if the arity of the inductive types are well formed *) List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;