diff options
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 773525ea43..f40cc5eee9 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -163,7 +163,7 @@ let explain_unexpected_type k ctx actual_type expected_type = let explain_not_product k ctx c = let ctx = make_all_name_different ctx in let pr = prterm_env ctx c in - [< 'sTR"This type of this term is expected to be a product but it is"; + [< 'sTR"The type of this term is expected to be a product but it is"; 'bRK(1,1); pr; 'fNL >] (* (co)fixpoints *) |