From 2c92d6fd70eb8752a732bb1f54cf64ef97ee444a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 18 Dec 2001 09:16:00 +0000
Subject: Nettoyage exceptions liées au vieux Case

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2304 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretype_errors.mli | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 5d04c50479..c3921f2452 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -20,13 +20,8 @@ open Inductiveops
 
 (*s The type of errors raised by the pretyper *)
 
-type ml_case_error =
-  | MlCaseAbsurd
-  | MlCaseDependent
-
 type pretype_error =
   (* Old Case *)
-  | MlCase of ml_case_error * inductive_type * unsafe_judgment
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of int * constr
@@ -61,9 +56,6 @@ val error_cant_apply_bad_type_loc :
   loc -> env ->  Evd.evar_map -> int * constr * constr -> 
       unsafe_judgment -> unsafe_judgment list -> 'b
 
-val error_cant_find_case_type_loc :
-  loc -> env ->  Evd.evar_map -> constr -> 'b
-
 val error_case_not_inductive_loc :
   loc -> env ->  Evd.evar_map -> unsafe_judgment -> 'b
 
@@ -87,9 +79,8 @@ val error_not_clean : env ->  Evd.evar_map -> int -> constr -> 'b
 
 (*s Ml Case errors *)
 
-val error_ml_case_loc :
-  loc -> env ->  Evd.evar_map ->
-      ml_case_error -> inductive_type -> unsafe_judgment -> 'b
+val error_cant_find_case_type_loc :
+  loc -> env ->  Evd.evar_map -> constr -> 'b
 
 (*s Pretyping errors *)
 
-- 
cgit v1.2.3