aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/typeops.ml')
-rw-r--r--kernel/typeops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index dbc0dcb73..1a07bb2fc 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -430,10 +430,10 @@ let rec execute env cstr =
(* Partial proofs: unsupported by the kernel *)
| Meta _ ->
- anomaly (Pp.str "the kernel does not support metavariables")
+ anomaly (Pp.str "the kernel does not support metavariables.")
| Evar _ ->
- anomaly (Pp.str "the kernel does not support existential variables")
+ anomaly (Pp.str "the kernel does not support existential variables.")
and execute_is_type env constr =
let t = execute env constr in