Remplacement du tableau du nombre d'args utiles pour la réduction des Cases par le nombre d'args inutiles + vérification dans le noyau

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

2 files changed, 14 insertions, 18 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index e29fab4e26..6f91ac5b8d 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -317,8 +317,11 @@ and cbv_stack_term info stack env t =
        (use red_under because we know there is a Case) *)
     | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,(arity,_),env,stk)))
             when red_under (info_flags info) fIOTA ->
+(*
 	let ncargs = arity.(n-1) in
 	let real_args = list_lastn ncargs args in
+*)
+	let real_args = snd (list_chop arity args) in
         cbv_stack_term info (stack_app real_args stk) env br.(n-1)
          
     (* constructor of arity 0 in a Case -> IOTA ( "   " )*)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 9ce397dd44..f2ffbbaf3b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -112,16 +112,15 @@ let encode_inductive id =
   let constr_lengths = Array.map List.length (mis_recarg mis) in
   (indsp,constr_lengths)
 
+let constr_nargs indsp =
+  let mis = Global.lookup_mind_specif (indsp,[||] (* ?? *)) in
+  Array.map List.length (mis_recarg mis)
+
 let sp_of_spi (refsp,tyi) =
   let mip = Declarations.mind_nth_type_packet (Global.lookup_mind refsp) tyi in
   let (pa,_,k) = repr_path refsp in 
   make_path pa mip.Declarations.mind_typename k
 
-(*
-  let (_,mip) = mind_specif_of_mind_light spi in
-  let (pa,_,k) = repr_path sp in 
-  make_path pa (mip.mind_typename) k
-*)
 (* Parameterization of the translation from constr to ast      *)
 
 (* Tables for Cases printing under a "if" form, a "let" form,  *)
@@ -129,20 +128,11 @@ let sp_of_spi (refsp,tyi) =
 let isomorphic_to_bool lc =
   Array.length lc = 2 & lc.(0) = 0 & lc.(1) = 0
 
-(*
-let isomorphic_to_bool lc =
-  let lcparams = Array.map get_params lc in
-  Array.length lcparams = 2 & lcparams.(0) = [] & lcparams.(1) = []
-*)
-
-let isomorphic_to_tuple lc = (Array.length lc = 1)
-(*
 let isomorphic_to_tuple lc = (Array.length lc = 1)
-*)
+
 module PrintingCasesMake =
   functor (Test : sig 
      val test : int array -> bool
-(*     val test : constr array -> bool*)
      val error_message : string
      val member_message : identifier -> bool -> string
      val field : string
@@ -195,8 +185,10 @@ module PrintingCasesLet =
 module PrintingIf  = Goptions.MakeIdentTable(PrintingCasesIf)
 module PrintingLet = Goptions.MakeIdentTable(PrintingCasesLet)
 
-let force_let (lc,(indsp,_,_,_,_)) = PrintingLet.active (indsp,lc)
-let force_if (lc,(indsp,_,_,_,_)) = PrintingIf.active (indsp,lc)
+let force_let (_,(indsp,_,_,_,_)) = 
+  let lc = constr_nargs indsp in PrintingLet.active (indsp,lc)
+let force_if (_,(indsp,_,_,_,_)) =
+  let lc = constr_nargs indsp in PrintingIf.active (indsp,lc)
 
 (* Options for printing or not wildcard and synthetisable types *)
 
@@ -311,7 +303,8 @@ let rec detype avoid env t =
     | IsMutCase (annot,p,c,bl) ->
 	let synth_type = synthetize_type () in
 	let tomatch = detype avoid env c in
-	let (consnargsl,(indsp,considl,k,style,tags)) = annot in
+	let (_,(indsp,considl,k,style,tags)) = annot in
+	let consnargsl = constr_nargs indsp in
 	let pred = 
 	  if synth_type & computable p k & considl <> [||] then
 	    None