diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 463a8bda4..c2a648301 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -643,7 +643,7 @@ type state = constr * constr Stack.t type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } +type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list @@ -825,7 +825,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies context" in contract_fix *) let reduce_and_refold_fix recfun env sigma refold cst_l fix sk = let raw_answer = - let env = if refold then None else Some env in + let env = if refold then Some env else None in contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in apply_subst (fun sigma x (t,sk') -> @@ -1496,7 +1496,7 @@ let instance sigma s c = let hnf_prod_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl @@ -1507,7 +1507,7 @@ let hnf_prod_applist env sigma t nl = let hnf_lam_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Lambda (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") + | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction.") let hnf_lam_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl @@ -1744,5 +1744,5 @@ let betazetaevar_applist sigma n c l = | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | Evar _, _ -> applist (substl env t, stack) - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in stacklam n [] c l |