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 8c5dcae76d0d700e5a93156faa32bdb5eae66ba0..d73b4fddb5345db76a5663bf717a63bff111ba47 100644 (file)
--- 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