From be800056397163ec9c475e6aee44925c97f86f58 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 24 Nov 1999 17:57:25 +0000
Subject: MAJ pour fusion avec pretyping

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/himsg.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'toplevel')

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
-- 
cgit v1.2.3