+let rec fire_projection_redex on_args = function
+ | C.Meta _ as t -> t
+ | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot->
+ let l= if on_args then List.map (fire_projection_redex true) ol else ol in
+ let t = if l == ol then ot else C.Appl l in
+ let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes r in
+ let conclude () =
+ if on_args then
+ let l' = HExtlib.sharing_map (fire_projection_redex true) l in
+ if l == l' then t else C.Appl l'
+ else
+ t (* ot is the same *)
+ in
+ if pragma <> `Projection || List.length args <= rno then conclude ()
+ else
+ (match List.nth args rno with
+ | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
+ let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
+ let t = C.Appl (fbody::args) in
+ (match NCicReduction.head_beta_reduce ~delta:max_int t with
+ | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])->
+ let _,kargs = HExtlib.split_nth leftno kargs in
+ fire_projection_redex false
+ (NCicReduction.head_beta_reduce
+ ~delta:max_int (C.Appl (pat :: kargs)))
+ | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) ->
+ let _,kargs = HExtlib.split_nth leftno kargs in
+ fire_projection_redex false
+ (NCicReduction.head_beta_reduce
+ ~delta:max_int (C.Appl (pat :: kargs @ args)))
+ | _ -> conclude ())
+ | _ -> conclude ())
+ | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t
+ | t -> t
+;;
+
+let apply_subst ?(fix_projections=false) subst context t =