diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index abbd47b8b1..16bd2b9c74 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -408,14 +408,27 @@ let internal_red_product env sigma c = let simpfun = clos_norm_flags (UNIFORM,betaiotazeta_red) env sigma in let rec redrec env x = match kind_of_term x with - | IsApp (f,l) -> simpfun (appvect (redrec env f, l)) + | IsApp (f,l) -> + (match kind_of_term f with + | IsFix fix -> + let stack = append_stack l empty_stack in + (match fix_recarg fix stack with + | None -> raise Redelimination + | Some (recargnum,recarg) -> + let recarg' = redrec env recarg in + let stack' = stack_assign stack recargnum recarg' in + simpfun (app_stack (f,stack'))) + | _ -> simpfun (appvect (redrec env f, l))) | IsCast (c,_) -> redrec env c | IsProd (x,a,b) -> mkProd (x, a, redrec (push_rel_assum (x,a) env) b) | IsLetIn (x,a,b,t) -> redrec env (subst1 a t) + | IsMutCase (ci,p,d,lf) -> simpfun (mkMutCase (ci,p,redrec env d,lf)) | _ when isEvalRef x -> + (* TO DO: re-fold fixpoints after expansion *) + (* to get true one-step reductions *) (match reference_opt_value sigma env (destEvalRef x) with | None -> raise Redelimination - | Some c -> simpfun c) + | Some c -> c) | _ -> raise Redelimination in redrec env c |