- normalize_machine ~delta ~subst ctx
- (fst (NCicReduction.reduce_machine ~delta ~subst ctx (0,[],t,[])))
-and normalize_machine ?(delta=0) ~subst ctx (k,e,t,s) =
- assert (delta=0);
- let t =
- if k = 0 then t
- else
- NCicSubstitution.psubst ~avoid_beta_redexes:true
- (fun e -> normalize_machine ~delta ~subst ctx (NCicReduction.from_env ~delta e)) e t in
- let t =
- match t with