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
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 ));
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;