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

13 files changed, 46 insertions, 106 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index ef52bd1cde..815bda4aa9 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -203,7 +203,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let branches=Array.init lp branch in
   let casee=mkRel 1 in
   let pred=mkLambda(Anonymous,intype,outtype) in
-  let case_info=make_default_case_info (pf_env gls) RegularStyle ind in
+  let case_info=make_case_info (pf_env gls) ind RegularStyle in
   let body= mkCase(case_info, pred, casee, branches) in
   let id=pf_get_new_id (id_of_string "t") gls in     
     mkLambda(Name id,intype,body)
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 7e18e58a04..b7243374b2 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -145,8 +145,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
 
@@ -468,25 +467,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 *)
 
@@ -544,7 +524,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 *)
@@ -1171,7 +1151,6 @@ let group_equations pb ind current cstrs mat =
 	       for i=1 to Array.length cstrs do
 		 let n = cstrs.(i-1).cs_nargs in
 		 let args = make_anonymous_patvars n 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,_) ->
@@ -1197,12 +1176,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 -> anomaly "Predicate not found"
     | 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 =
@@ -1324,23 +1303,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 =
@@ -1349,8 +1326,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 }
 
@@ -1376,8 +1352,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
@@ -1397,7 +1372,6 @@ let matx_of_eqns env eqns =
 	it = rhs;
       } in
     { patterns = lpat;
-      tag = RegularPat;
       alias_stack = [];
       eqn_loc = loc;
       used = ref false;
@@ -2089,7 +2063,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;
 	let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
@@ -2118,7 +2092,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;
 	  let j = { j with uj_val = it_mkLambda_or_LetIn j.uj_val tomatchs_lets } in
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index e53dad2659..990ee115f6 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -397,7 +397,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let v =
 		       let mis,_ = dest_ind_family indf in
-		       let ci = make_default_case_info env LetStyle mis in
+		       let ci = make_case_info env mis LetStyle in
 			 mkCase (ci, p, cj.uj_val,[|f|]) in 
 		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
 
@@ -415,7 +415,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 		     let v =
 		       let mis,_ = dest_ind_family indf in
-		       let ci = make_default_case_info env LetStyle mis in
+		       let ci = make_case_info env mis LetStyle in
 			 mkCase (ci, p, cj.uj_val,[|f|] ) 
 		     in
 		       { uj_val = v; uj_type = ccl })
@@ -485,7 +485,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  let b2 = f cstrs.(1) b2 in
 	  let v =
 	    let mis,_ = dest_ind_family indf in
-	    let ci = make_default_case_info env IfStyle mis in
+	    let ci = make_case_info env mis IfStyle in
 	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
 	  in
 	    { uj_val = v; uj_type = p }
diff --git a/kernel/term.ml b/kernel/term.ml
index 49d4d231b5..6a0fe60f61 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -24,12 +24,10 @@ type metavariable = int
 (* This defines the strategy to use for verifiying a Cast *)
 
 (* This defines Cases annotations *)
-type pattern_source = DefaultPat of int | RegularPat
 type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
 type case_printing =
   { ind_nargs : int; (* number of real args of the inductive type *)
-    style     : case_style;
-    source    : pattern_source array }
+    style     : case_style }
 type case_info =
   { ci_ind        : inductive;
     ci_npar       : int;
diff --git a/kernel/term.mli b/kernel/term.mli
index 1b19f83f41..0d40da9691 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -40,12 +40,10 @@ type existential_key = int
 type metavariable = int
 
 (*s Case annotation *)
-type pattern_source = DefaultPat of int | RegularPat
 type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
 type case_printing =
   { ind_nargs : int; (* number of real args of the inductive type *)
-    style     : case_style;
-    source    : pattern_source array }
+    style     : case_style }
 (* the integer is the number of real args, needed for reduction *)
 type case_info =
   { ci_ind        : inductive;
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
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 88bb055dcc..7fd65050c5 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -78,7 +78,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
       let depind = build_dependent_inductive env indf' in
       let deparsign = (Anonymous,None,depind)::arsign in
 
-      let ci = make_default_case_info env RegularStyle ind in
+      let ci = make_case_info env ind RegularStyle in
       let pbody =
         appvect
           (mkRel (ndepar + nbprod),
@@ -350,7 +350,7 @@ let mis_make_indrec env sigma listdepkind mib =
 
 	    (* body of i-th component of the mutual fixpoint *)
 	    let deftyi = 
-	      let ci = make_default_case_info env RegularStyle indi in
+	      let ci = make_case_info env indi RegularStyle in
 	      let concl = applist (mkRel (dect+j+ndepar),pargs) in 
 	      let pred =
 		it_mkLambda_or_LetIn_name env 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 041187d84f..69f921b790 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -131,21 +131,16 @@ let allowed_sorts env (kn,i as ind) =
   mip.mind_kelim
 
 (* Annotation for cases *)
-let make_case_info env ind style pats_source =
+let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let print_info =
-    { ind_nargs = mip.mind_nrealargs;
-      style     = style;
-      source    = pats_source } in
+  let print_info = { ind_nargs = mip.mind_nrealargs; style = style } in
   { ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
     ci_cstr_nargs = mip.mind_consnrealdecls;
     ci_pp_info = print_info }
 
 let make_default_case_info env style ind =
-  let (mib,mip) = Inductive.lookup_mind_specif env ind in
   make_case_info env ind style
-    (Array.map (fun _ -> RegularPat) mip.mind_consnames)
 
 (*s Useful functions *)
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 8285b81670..3cc24a184f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -105,9 +105,11 @@ val arity_of_case_predicate :
 val type_case_branches_with_names :
   env -> inductive * constr list -> unsafe_judgment -> constr ->
     types array * types
-val make_case_info :
-  env -> inductive -> case_style -> pattern_source array -> case_info
+val make_case_info : env -> inductive -> case_style -> case_info
+
+(*i Compatibility 
 val make_default_case_info : env -> case_style -> inductive -> case_info
+i*)
 
 (********************)
 val control_only_guard : env -> types -> unit
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 81bd6987fe..dc3ea869c1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -479,7 +479,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let v =
 		       let mis,_ = dest_ind_family indf in
-		       let ci = make_default_case_info env LetStyle mis in
+		       let ci = make_case_info env mis LetStyle in
 			 mkCase (ci, p, cj.uj_val,[|f|]) in 
 		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
 
@@ -498,7 +498,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 		     let v =
 		       let mis,_ = dest_ind_family indf in
-		       let ci = make_default_case_info env LetStyle mis in
+		       let ci = make_case_info env mis LetStyle in
 			 mkCase (ci, p, cj.uj_val,[|f|] ) 
 		     in
 		       { uj_val = v; uj_type = ccl })
@@ -568,7 +568,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  let b2 = f cstrs.(1) b2 in
 	  let v =
 	    let mis,_ = dest_ind_family indf in
-	    let ci = make_default_case_info env IfStyle mis in
+	    let ci = make_case_info env mis IfStyle in
 	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
 	  in
 	    { uj_val = v; uj_type = p }
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 7c149e9647..d86b2c07de 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -553,7 +553,7 @@ e types")
         let cl' = replace_vars [id1,mkVar id2] cl in
           ([mk_goal sign' cl'], sigma)
 
-    | Change_evars as r ->
+    | Change_evars ->
         match norm_goal sigma goal with
 	    Some ngl -> ([ngl],sigma)
           | None -> ([goal], sigma)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9ca5dabdcb..e2b3ec57c2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -397,7 +397,7 @@ let descend_then sigma env head dirn =
       let brl =
         List.map build_branch
           (interval 1 (Array.length mip.mind_consnames)) in
-      let ci = make_default_case_info env RegularStyle ind in
+      let ci = make_case_info env ind RegularStyle in
       mkCase (ci, p, head, Array.of_list brl)))
   
 (* Now we need to construct the discriminator, given a discriminable
@@ -440,7 +440,7 @@ let construct_discriminator sigma env dirn c sort =
     it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in
   let brl =
     List.map build_branch(interval 1 (Array.length mip.mind_consnames)) in
-  let ci = make_default_case_info env RegularStyle ind in
+  let ci = make_case_info env ind RegularStyle in
   mkCase (ci, p, c, Array.of_list brl)
     
 let rec build_discriminator sigma env dirn c sort = function
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 28ecb909a2..f3ec4732d7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -152,8 +152,7 @@ let declare_projections indsp coers fields =
 		let ccl' = liftn 1 2 ccl in
 		let p = mkLambda (x, lift 1 rp, ccl') in
 		let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
-		let ci = Inductiveops.make_case_info env indsp
-		  LetStyle [| RegularPat |] in
+		let ci = Inductiveops.make_case_info env indsp LetStyle in
 		mkCase (ci, p, mkRel 1, [|branch|]) in
 	      let proj =
 	        it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in