diff options
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 82f09cf4b..ba0b01784 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -333,13 +333,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* Eta-expansion on the fly *) | (FLambda _, _) -> if v1 <> [] then - anomaly (Pp.str "conversion was given unreduced term (FLambda)"); + anomaly (Pp.str "conversion was given unreduced term (FLambda)."); let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr univ CONV infos (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2)) | (_, FLambda _) -> if v2 <> [] then - anomaly (Pp.str "conversion was given unreduced term (FLambda)"); + anomaly (Pp.str "conversion was given unreduced term (FLambda)."); let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr univ CONV infos (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[])) @@ -479,7 +479,7 @@ let vm_conv cv_pb = fconv cv_pb true let hnf_prod_app env t n = match whd_all env 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_applist env t nl = List.fold_left (hnf_prod_app env) t nl |