Suppression argument pattern_source du case_info (code jamais utilisé)

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

1 files changed, 12 insertions, 38 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index eb2d88f3d8..f8c8e0a138 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -142,8 +142,7 @@ type equation =
       rhs          : rhs;
       alias_stack  : name list;
       eqn_loc      : loc;
-      used         : bool ref;
-      tag          : pattern_source }
+      used         : bool ref }
 
 type matrix = equation list
 
@@ -460,25 +459,6 @@ let remove_current_pattern eqn =
 let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns }
 
 (**********************************************************************)
-(* Dealing with regular and default patterns *)
-let is_regular eqn = eqn.tag = RegularPat
-
-let lower_pattern_status = function
-  | RegularPat -> DefaultPat 0
-  | DefaultPat n -> DefaultPat (n+1)
-
-let pattern_status pats =
-  if array_exists ((=) RegularPat) pats then RegularPat
-  else 
-    let min =
-      Array.fold_right
-	(fun pat n -> match pat with
-	   | DefaultPat i when i<n -> i
-	   | _ -> n)
-	pats 0 in
-    DefaultPat min
-
-(**********************************************************************)
 (* Well-formedness tests *)
 (* Partial check on patterns *)
 
@@ -536,7 +516,7 @@ let extract_rhs pb =
     | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
     | eqn::_ ->
 	set_used_pattern eqn;
-	eqn.tag, eqn.rhs
+        eqn.rhs
 
 (**********************************************************************)
 (* Functions to deal with matrix factorization *)
@@ -1139,7 +1119,6 @@ let group_equations pb ind current cstrs mat =
 	       (* This is a default clause that we expand *)
 	       for i=1 to Array.length cstrs do
 		 let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in
-		 let rest = {rest with tag = lower_pattern_status rest.tag} in
 		 brs.(i-1) <- (args, rest) :: brs.(i-1)
 	       done
 	   | PatCstr (loc,((_,i)),args,_) ->
@@ -1165,12 +1144,12 @@ let rec generalize_problem pb = function
 
 (* No more patterns: typing the right-hand-side of equations *)
 let build_leaf pb =
-  let tag, rhs = extract_rhs pb in
+  let rhs = extract_rhs pb in
   let tycon = match pb.pred with
     | None -> empty_tycon
     | Some (PrCcl typ) -> mk_tycon typ
     | Some _ -> anomaly "not all parameters of pred have been consumed" in
-  tag, pb.typing_function tycon rhs.rhs_env rhs.it
+  pb.typing_function tycon rhs.rhs_env rhs.it
 
 (* Building the sub-problem when all patterns are variables *)
 let shift_problem (current,t) pb =
@@ -1292,23 +1271,21 @@ and match_current pb tomatch =
 	  let brs = array_map2 (compile_branch current deps pb) eqns cstrs in
 
 	  (* We build the (elementary) case analysis *)
-	  let tags   = Array.map (fun (t,_,_) -> t) brs in
-	  let brvals = Array.map (fun (_,v,_) -> v) brs in
-	  let brtyps = Array.map (fun (_,_,t) -> t) brs in
+	  let brvals = Array.map (fun (v,_) -> v) brs in
+	  let brtyps = Array.map (fun (_,t) -> t) brs in
 	  let (pred,typ,s) =
 	    find_predicate pb.caseloc pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt pb.tomatch in
-	  let ci = make_case_info pb.env mind RegularStyle tags in
+	  let ci = make_case_info pb.env mind RegularStyle in
 	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
 	  let inst = List.map mkRel deps in
-	  pattern_status tags,
 	  { uj_val = applist (case, inst);
 	    uj_type = substl inst typ }
 
 and compile_branch current deps pb eqn cstr =
   let sign, pb = build_branch current deps pb eqn cstr in
-  let tag, j = compile pb in
-  (tag, it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
+  let j = compile pb in
+  (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
 
 and compile_generalization pb d rest =
   let pb =
@@ -1317,8 +1294,7 @@ and compile_generalization pb d rest =
        tomatch = rest;
        pred = option_map ungeneralize_predicate pb.pred;
        mat = List.map (push_rels_eqn [d]) pb.mat } in
-  let patstat,j = compile pb in
-  patstat, 
+  let j = compile pb in
   { uj_val = mkLambda_or_LetIn d j.uj_val;
     uj_type = mkProd_or_LetIn d j.uj_type }
 
@@ -1344,8 +1320,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
        pred = option_map (lift_predicate n) pb.pred;
        history = history;
        mat = mat } in
-  let patstat,j = compile pb in
-  patstat, 
+  let j = compile pb in
   List.fold_left mkSpecialLetInJudge j sign
 
 (* pour les alias des initiaux, enrichir les env de ce qu'il faut et
@@ -1366,7 +1341,6 @@ let matx_of_eqns env tomatchl eqns =
 	avoid_ids = ids@(ids_of_named_context (named_context env));
 	it = initial_rhs } in
     { patterns = initial_lpat;
-      tag = RegularPat;
       alias_stack = [];
       eqn_loc = loc;
       used = ref false;
@@ -1632,7 +1606,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
       caseloc  = loc;
       typing_function = typing_fun } in
     
-  let _, j = compile pb in
+  let j = compile pb in
     (* We check for unused patterns *)
     List.iter (check_unused_pattern env) matx;
     inh_conv_coerce_to_tycon loc env isevars j tycon