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

1 files changed, 5 insertions, 13 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7f6f05d11b..a05cc767cb 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -131,9 +131,13 @@ let build_notdep_pred env sigma indf pred =
   let nar = List.length arsign in
   it_mkLambda_or_LetIn_name env (lift nar pred) arsign
 
+type ml_case_error =
+  | MlCaseAbsurd
+  | MlCaseDependent
+
 exception NotInferable of ml_case_error
 
-let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) =
+let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) =
   let pred =
     let (ind,params) = indf in
     let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -154,18 +158,6 @@ let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) =
   else (* we try with [_:T1]..[_:Tn](lift n pred) *)
     build_notdep_pred env sigma indf pred  
 
-let pred_case_ml loc env sigma isrec indt lf (i,ft) = 
-  try pred_case_ml_fail env sigma isrec indt (i,ft)
-  with NotInferable e ->
-    let j = {uj_val=lf.(i-1); uj_type=ft} in
-    error_ml_case_loc loc env sigma e indt j
-
-(* similar to pred_case_ml but does not expect the list lf of braches *)
-let pred_case_ml_onebranch loc env sigma isrec indt (i,fj) = 
-  try pred_case_ml_fail env sigma isrec indt (i,fj.uj_type)
-  with NotInferable e ->
-    error_ml_case_loc loc env sigma e indt fj
-
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
 (************************************************************************)