diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
| commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
| tree | e035f490e2c748356df73342876b22cfcb3bc5a0 /checker/reduction.ml | |
| parent | 5e8824960f68f529869ac299b030282cc916ba2c (diff) | |
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
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 c2d5c261c..57e39f9ce 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -287,13 +287,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* Eta-expansion on the fly *) | (FLambda _, _) -> if v1 <> [] then - anomaly "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 "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,[])) @@ -398,7 +398,7 @@ let vm_conv = fconv let hnf_prod_app env t n = match whd_betadeltaiota env t with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly "hnf_prod_app: 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 |