diff options
| author | herbelin | 2001-12-19 11:01:30 +0000 |
|---|---|---|
| committer | herbelin | 2001-12-19 11:01:30 +0000 |
| commit | bed2c40991d7a49ab4e8435a38d6bd0708f7011a (patch) | |
| tree | 41fa92426293293983357517389d9a27230a6b34 /toplevel | |
| parent | d3d8e2b31e71dfa87ce747e410f974a51a4fa272 (diff) | |
Corrections post contournement des streams avec ++
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2332 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/fhimsg.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index c5294c0b70..55c45dd4d1 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -267,15 +267,15 @@ let explain_ml_case k ctx mes c ct br brt = | "Decomp" -> let plf = P.pr_term k ctx br in let pft = P.pr_term k ctx brt in - (str "The branch " ++ plf ++ 'wS 1 ++ cut () ++ str "has type " ++ pft ++ - 'wS 1 ++ cut () ++ + (str "The branch " ++ plf ++ ws 1 ++ cut () ++ str "has type " ++ pft ++ + ws 1 ++ cut () ++ str "does not correspond to the inductive definition") | "Dependent" -> (str "ML case not allowed for a dependent case elimination") | _ -> (mt ()) in - hov 0 (str "In ML case expression on " ++ pc ++ 'wS 1 ++ cut () ++ - str "of type" ++ 'wS 1 ++ pct ++ 'wS 1 ++ cut () ++ + hov 0 (str "In ML case expression on " ++ pc ++ ws 1 ++ cut () ++ + str "of type" ++ ws 1 ++ pct ++ ws 1 ++ cut () ++ str "which is an inductive predicate." ++ fnl () ++ expln) (* let explain_cant_find_case_type loc k ctx c = @@ -283,7 +283,7 @@ let explain_cant_find_case_type loc k ctx c = Ast.user_err_loc (loc,"pretype", hov 3 (str "Cannot infer type of whole Case expression on" ++ - 'wS 1 ++ pe)) + ws 1 ++ pe)) *) let explain_type_error k ctx = function | UnboundRel n -> |