diff options
| -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 |