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 /kernel/vm.ml | |
| parent | b377bd30f23f430882902f534eaf31b1314ecd07 (diff) | |
| parent | 88fdd28815747520bdc555a2d1b8600e114ab341 (diff) | |
Merge PR#716: Don't double up on periods in anomalies
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index 53483a2220..21c1225cc4 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -236,7 +236,7 @@ let uni_lvl_val (v : values) : Univ.universe_level = in CErrors.anomaly Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr) + ++ pr ++ str ".") let rec whd_accu a stk = let stk = @@ -285,7 +285,7 @@ let rec whd_accu a stk = end | tg -> CErrors.anomaly - Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg) + Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" @@ -308,7 +308,7 @@ let whd_val : values -> whd = | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) else Vconstr_block(Obj.obj o) |