From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 14 Apr 2009 16:37:40 +0000 (+0000)
Subject: Trick: the refiner always subst-expands the outtype, so that the beta-redex
X-Git-Tag: make_still_working~4084
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=281f0c7b4fc0d5b97025625af2ecff85edebbb5c;p=helm.git

Trick: the refiner always subst-expands the outtype, so that the beta-redex
that will be formed will always be reduced by substitution.
---

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