diff options
| author | herbelin | 1999-12-15 17:05:01 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-15 17:05:01 +0000 |
| commit | e16cd2776ab7c779657bd73c58e0f77385c9e16f (patch) | |
| tree | 297c87cd98c396c2b9a8580dfd0dd3daf3a58bd3 | |
| parent | 0e414a3c707d62e9d19443fe9256168a4eeca116 (diff) | |
message erreur Scheme
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@259 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/command.ml | 3 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index ce804aa7f2..04fdd2e399 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -341,7 +341,8 @@ let inductive_of_ident id = let c = try global_reference CCI id with Not_found -> - errorlabstrm "inductive_of_ident" ((string_of_id id) ^ " not found") + errorlabstrm "inductive_of_ident" + [< 'sTR ((string_of_id id) ^ " not found") >] in match kind_of_term (global_reference CCI id) with | IsMutInd ind -> ind diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 78709719ab..3df7d1d0fb 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -89,7 +89,7 @@ let explain_ill_formed_branch k ctx c i actty expty = [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc; 'sPC; 'sTR "the branch " ; 'iNT (i+1); 'sTR " has type"; 'bRK(1,1); pa ; 'sPC; - 'sTR "which should be:"; 'bRK(1,1); pe >] + 'sTR "which should be"; 'bRK(1,1); pe >] let explain_generalization k ctx (name,var) c = let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in |