aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/modutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/modutil.ml')
-rw-r--r--plugins/extraction/modutil.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 60fe8e7620..b67b9931ec 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -19,7 +19,7 @@ open Mlutil
let rec msid_of_mt = function
| MTident mp -> mp
| MTwith(mt,_)-> msid_of_mt mt
- | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name")
+ | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name.")
(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
[ml_structure]. *)
@@ -231,7 +231,7 @@ let get_decl_in_structure r struc =
| _ -> error_not_visible r
in go ll sel
with Not_found ->
- anomaly (Pp.str "reference not found in extracted structure")
+ anomaly (Pp.str "reference not found in extracted structure.")
(*s Optimization of a [ml_structure]. *)