pretyping/pretyping.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2986 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 0 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a64c3b800..63b310bc3 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -26,6 +26,7 @@ open Cases
 open Logic
 open Printer
 open Ast
+open Rawterm
 
 let guill s = "\""^s^"\""
 
@@ -278,6 +279,24 @@ let explain_not_clean ctx ev t =
   str" with a term using variable " ++ var ++ spc () ++
   str"which is not in its scope."
 
+let explain_unsolvable_implicit env = function
+  | QuestionMark -> str "Cannot infer a term for this placeholder"
+  | CasesType ->
+      str "Cannot infer the type of this pattern-matching problem"
+  | AbstractionType (Name id) ->
+      str "Cannot infer a type for " ++ Nameops.pr_id id
+  | AbstractionType Anonymous ->
+      str "Cannot infer a type of this anonymous abstraction"
+  | ImplicitArg (c,n) ->
+      str "Cannot infer the " ++ pr_ord n ++
+      str " implicit argument of " ++ Nametab.pr_global_env None c
+  | InternalHole ->
+      str "Cannot infer a term for an internal placeholder"
+  | TomatchTypeParameter (tyi,n) ->
+      str "Cannot infer the " ++ pr_ord n ++
+      str " argument of the inductive type (" ++ pr_inductive env tyi ++
+      str ") of this term"
+
 let explain_var_not_found ctx id = 
   str "The variable" ++ spc () ++ str (string_of_id id) ++
   spc ()  ++ str "was not found" ++ 
@@ -339,6 +358,8 @@ let explain_pretype_error ctx = function
       explain_occur_check ctx n c
   | NotClean (n,c) ->
       explain_not_clean ctx n c
+  | UnsolvableImplicit k ->
+      explain_unsolvable_implicit ctx k
   | VarNotFound id ->
       explain_var_not_found ctx id
   | UnexpectedType (actual,expected) ->