diff options
| author | Maxime Dénès | 2017-06-06 00:24:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 00:24:57 +0200 |
| commit | cc0f9d254c394db742473299336fb20b82ae4aa1 (patch) | |
| tree | cbc89906c862624d4285f367d1fa9f0f61f16f05 /pretyping/reductionops.ml | |
| parent | b377bd30f23f430882902f534eaf31b1314ecd07 (diff) | |
| parent | 88fdd28815747520bdc555a2d1b8600e114ab341 (diff) | |
Merge PR#716: Don't double up on periods in anomalies
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5a2328aaa4..c976fe66dd 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1445,7 +1445,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 @@ -1456,7 +1456,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 @@ -1693,5 +1693,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 |