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

5 files changed, 20 insertions, 51 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7f6f05d11..a05cc767c 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)                      *)
 (************************************************************************)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 222300028..45694a01b 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -30,15 +30,21 @@ type pattern_matching_error =
 
 exception PatternMatchingError of env * pattern_matching_error
 
-(* Used for old cases in pretyping *)
+(*s Used for old cases in pretyping *)
 
 val branch_scheme : 
   env -> evar_defs -> bool -> inductive * constr list -> constr array
 
-val pred_case_ml_onebranch : loc -> env -> evar_map -> bool ->
-  inductive_type -> int * unsafe_judgment -> constr 
+type ml_case_error =
+  | MlCaseAbsurd
+  | MlCaseDependent
 
-(* Compilation of pattern-matching. *)
+exception NotInferable of ml_case_error
+
+val pred_case_ml : (* raises [NotInferable] if not inferable *)
+  env -> evar_map -> bool -> inductive_type -> int * types -> constr 
+
+(*s Compilation of pattern-matching. *)
 
 val compile_cases :
   loc -> (type_constraint -> env -> rawconstr -> unsafe_judgment)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 034597a71..cc8b0ed8b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -18,13 +18,8 @@ open Type_errors
 open Rawterm
 open Inductiveops
 
-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
@@ -108,10 +103,6 @@ let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
        ((n,nf_evar sigma c, nf_evar sigma t),
         j_nf_evar sigma rator, ja))
 
-let error_cant_find_case_type_loc loc env sigma expr =
-  raise_pretype_error
-    (loc, env, sigma, CantFindCaseType (nf_evar sigma expr))
-
 let error_ill_formed_branch_loc loc env sigma c i actty expty =
   let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
   raise_located_type_error
@@ -146,9 +137,9 @@ let error_not_clean env sigma ev c =
 
 (*s Ml Case errors *)
 
-let error_ml_case_loc loc env sigma mes indt j =
+let error_cant_find_case_type_loc loc env sigma expr =
   raise_pretype_error
-    (loc, env, sigma, MlCase (mes, indt, j_nf_evar sigma j))
+    (loc, env, sigma, CantFindCaseType (nf_evar sigma expr))
 
 (*s Pretyping errors *)
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 5d04c5047..c3921f245 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 *)
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4af71a587..2582057eb 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -256,18 +256,9 @@ let explain_not_inductive ctx c =
   str"The term" ++ brk(1,1) ++ pc ++ spc () ++
   str "is not an inductive definition"
 
-let explain_ml_case ctx mes =
-  let expln = match mes with
-    | MlCaseAbsurd ->
-	str "Unable to infer a predicate for an elimination an empty type"
-    | MlCaseDependent ->
-        str "Unable to infer a dependent elimination predicate"
-  in
-  hov 0 (str "Cannot infer ML Case predicate:" ++ fnl () ++ expln)
-
 let explain_cant_find_case_type ctx c =
   let pe = prterm_env ctx c in
-  hov 3 (str "Cannot infer type of whole Case expression on" ++ ws 1 ++ pe)
+  hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe)
 
 let explain_occur_check ctx ev rhs =
   let id = "?" ^ string_of_int ev in
@@ -338,8 +329,6 @@ let explain_type_error ctx = function
       explain_not_inductive ctx c
 *)
 let explain_pretype_error ctx = function
-  | MlCase (mes,_,_) ->
-      explain_ml_case ctx mes
   | CantFindCaseType c ->
       explain_cant_find_case_type ctx c
   | OccurCheck (n,c) ->