MAJ pour fusion avec pretyping

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

1 files changed, 8 insertions, 1 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 07c35ab32..53b35ff6d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -212,7 +212,14 @@ let explain_ml_case k ctx mes c ct br brt =
   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 =
+  let pe = P.pr_term k ctx c in
+  Ast.user_err_loc
+    (loc,"pretype",
+     hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 
+	     'wS 1; pe >])
+*)
 let explain_type_error k ctx = function
   | UnboundRel n -> 
       explain_unbound_rel k ctx n