X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=d73b4fddb5345db76a5663bf717a63bff111ba47;hb=e085135177f7b3b74b410d47a4f3bca1784b60b1;hp=8c5dcae76d0d700e5a93156faa32bdb5eae66ba0;hpb=d7f32114f3806b51c2ee483dcb5a86e08d086a72;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 8c5dcae76..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