bug correction in the decomposition of an induction scheme.

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

1 files changed, 57 insertions, 53 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c621f0200..8f4d85812 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1489,7 +1489,7 @@ let decompose_paramspred_branch_args elimt =
     match kind_of_term elimt with
       | Prod(nme,tpe,elimt')  -> 
 	  let hd_tpe,_ = decompose_app 
-	    (if isProd tpe then snd (decompose_prod tpe) else tpe) in
+	    (if isProd tpe then snd (decompose_prod_assum tpe) else tpe) in
 	  if not (occur_rel 1 elimt') && isRel hd_tpe	    
 	  then cut_noccur elimt' ((nme,None,tpe)::acc2)
 	  else 
@@ -1545,18 +1545,17 @@ let exchange_hd_app subst_hd t =
    (HI: I prm1..prmp x1...xni)                         (optional main induction arg)
    -> (Qi x1...xni HI        (f prm1...prmp x1...xni)).(conclusion)
                    ^^        ^^^^^^^^^^^^^^^^^^^^^^^^
-               optional                optional
-               even if HI      argument added if principle
-             present above   generated by functional induction
-             [indarg]          [farg]
+               optional        optional argument added if
+               even if HI    principle generated by functional 
+             present above   induction, only if HI does not exist
+             [indarg]                  [farg]
 
   HI is not present when the induction principle does not come directly from an
   inductive type (like when it is generated by functional induction for
   example). HI is present otherwise BUT may not appear in the conclusion
   (dependent principle). HI and (f...) cannot be both present.
 
-  Principles taken from functional induction have the final (f...).
-*)
+  Principles taken from functional induction have the final (f...).*)
 
 (* [rel_contexts] and [rel_declaration] actually contain triples, and
    lists are actually in reverse order to fit [compose_prod]. *)
@@ -1780,49 +1779,6 @@ let find_elim_signature isrec elim hyp0 gl =
   (indsign,elim_scheme)
 
 
-let induction_from_context isrec elim_info hyp0 names gl =
-  (*test suivant sans doute inutile car refait par le letin_tac*)
-  if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
-    errorlabstrm "induction" 
-      (str "Cannot generalize a global variable");
-  let indsign,scheme = elim_info in
-
-  let indref = match scheme.indref with | None -> assert false | Some x -> x in
-  let tmptyp0 =	pf_get_hyp_typ gl hyp0 in
-  let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
-
-  let env = pf_env gl in
-  let indvars = find_atomic_param_of_ind scheme.nparams (snd (decompose_prod typ0)) in
-  let statlists,lhyp0,indhyps,deps = cook_sign (Some hyp0) indvars env in
-  let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
-  let names = compute_induction_names (Array.length indsign) names in
-  let dephyps = List.map (fun (id,_,_) -> id) deps in
-  let deps_cstr =
-    List.fold_left
-      (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in
-
-  (* Magistral effet de bord: si hyp0 a des arguments, ceux d'entre
-     eux qui ouvrent de nouveaux buts arrivent en premier dans la
-     liste des sous-buts du fait qu'ils sont le plus ŕ gauche dans le
-     combinateur engendré par make_case_gen (un "Cases (hyp0 ?) of
-     ...")  et il faut alors appliquer tclTHENLASTn; en revanche,
-     comme lookup_eliminator renvoie un combinateur de la forme
-     "ind_rec ... (hyp0 ?)", les buts correspondant ŕ des arguments de
-     hyp0 sont maintenant ŕ la fin et c'est tclTHENFIRSTn qui marche !!! *)
-  tclTHENLIST
-    [ if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr;
-      thin dephyps;
-      (if isrec then tclTHENFIRSTn else tclTHENLASTn)
-       	(tclTHENLIST
-	  [ induction_tac hyp0 typ0 (scheme.elimc,scheme.elimt);
-	    thin [hyp0];
-            tclTRY (thin indhyps) ])
-       	(array_map2
-	   (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names)
-    ]
-    gl
-
-
 let mapi f l =
   let rec mapi_aux f i l =   
     match l with
@@ -1907,13 +1863,14 @@ let induction_from_context_l isrec elim_info lid names gl =
 	    + (if scheme.indarg <> None then 1 else 0) in
 	  let ivs,lp = cut_list nargs_without_indarg l in
 	  e, ivs, lp in
-  let statlists,lhyp0,indhyps,deps = cook_sign None (hyp0::indvars) env in
+  let statlists,lhyp0,indhyps,deps = 
+    (* if scheme.indarg<>None then cook_sign (Some hyp0) indvars env 
+    else *) cook_sign None (hyp0::indvars) env in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let names = compute_induction_names (Array.length indsign) names in
   let dephyps = List.map (fun (id,_,_) -> id) deps in
   let deps_cstr =
-    List.fold_left
-      (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in
+    List.fold_left (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in
   (* terms to patternify we must patternify indarg or farg if present in concl *)
   let lid_in_pattern = 
     if scheme.indarg <> None & not scheme.indarg_in_concl then indvars
@@ -1944,6 +1901,53 @@ let induction_from_context_l isrec elim_info lid names gl =
     ]
     gl
 
+
+
+let induction_from_context isrec elim_info hyp0 names gl =
+  (*test suivant sans doute inutile car refait par le letin_tac*)
+  if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
+    errorlabstrm "induction" 
+      (str "Cannot generalize a global variable");
+  let indsign,scheme = elim_info in
+
+  let indref = match scheme.indref with | None -> assert false | Some x -> x in
+  let tmptyp0 =	pf_get_hyp_typ gl hyp0 in
+  let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
+
+  let env = pf_env gl in
+  let indvars = find_atomic_param_of_ind scheme.nparams (snd (decompose_prod typ0)) in
+  (* induction_from_context_l isrec elim_info (hyp0::List.rev indvars) names gl  *)
+  let statlists,lhyp0,indhyps,deps = cook_sign (Some hyp0) indvars env in
+  let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
+  let names = compute_induction_names (Array.length indsign) names in
+  let dephyps = List.map (fun (id,_,_) -> id) deps in
+  let deps_cstr =
+    List.fold_left
+      (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in
+
+  (* Magistral effet de bord: si hyp0 a des arguments, ceux d'entre
+     eux qui ouvrent de nouveaux buts arrivent en premier dans la
+     liste des sous-buts du fait qu'ils sont le plus ŕ gauche dans le
+     combinateur engendré par make_case_gen (un "Cases (hyp0 ?) of
+     ...")  et il faut alors appliquer tclTHENLASTn; en revanche,
+     comme lookup_eliminator renvoie un combinateur de la forme
+     "ind_rec ... (hyp0 ?)", les buts correspondant ŕ des arguments de
+     hyp0 sont maintenant ŕ la fin et c'est tclTHENFIRSTn qui marche !!! *)
+  tclTHENLIST
+    [ if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr;
+      thin dephyps;
+      (if isrec then tclTHENFIRSTn else tclTHENLASTn)
+       	(tclTHENLIST
+	  [ induction_tac hyp0 typ0 (scheme.elimc,scheme.elimt);
+	    thin [hyp0];
+            tclTRY (thin indhyps) ])
+       	(array_map2
+	   (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names)
+    ]
+    gl
+
+
+
 exception TryNewInduct
 
 let induction_with_atomization_of_ind_arg isrec elim names hyp0 gl =