- | 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 ()
+ | C.Appl((C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r) as hd)::args) as ot->
+ let args'= HExtlib.sharing_map (fire_projection_redex status ()) args in
+ let t = if args == args' then ot else C.Appl (hd::args') in
+ let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
+ if pragma <> `Projection || List.length args <= rno then t