From 281f0c7b4fc0d5b97025625af2ecff85edebbb5c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 14 Apr 2009 16:37:40 +0000 Subject: [PATCH] Trick: the refiner always subst-expands the outtype, so that the beta-redex that will be formed will always be reduced by substitution. --- .../components/ng_refiner/nCicRefiner.ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) 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 -- 2.39.2