diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-15 16:42:18 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-15 16:42:18 +0000 |
| commit | f451038d4cf063ae5fb2dece1f95ec805482f4a1 (patch) | |
| tree | c0d449a88f4225c38a7321c90b5ee3c04a52fb26 | |
| parent | 44e7cd6dd3d4f50391c20bd27176fff30e1da33c (diff) | |
Expression anglaise
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@609 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 773525ea4..f40cc5eee 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 *) |