Problèmes de NewInduction

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

1 files changed, 21 insertions, 10 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b592fb759..247b9f07e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1268,18 +1268,29 @@ let induction_tac varname typ (elimc,elimt) gl =
   let elimclause = make_clenv_binding wc (mkCast (elimc,elimt),elimt) [] in
   elimination_clause_scheme kONT wc elimclause indclause gl
 
+let is_indhyp p n t =
+  let c,_ = decomp_app t in 
+  match kind_of_term c with
+    | IsRel k when p < k & k <= p + n -> true
+    | _ -> false
+
+(* We check that the eliminator has been build by Coq (usual *)
+(* eliminator _ind, _rec or _rect, or eliminator built by Scheme) *)
 let compute_elim_signature_and_roughly_check elimt mind =
   let mis = Global.lookup_mind_specif mind in
   let lra = mis_recarg mis in
   let nconstr = mis_nconstr mis in
-  let rec check_branch c ra = match kind_of_term c, ra with
-    | IsProd (_,_,c), Declarations.Mrec _ :: ra' ->
+  let _,elimt2 = decompose_prod_n (mis_nparams mis) elimt in
+  let n = nb_prod elimt2 in
+  let npred = n - nconstr - (mis_nrealargs mis) - 1 in
+  let rec check_branch p c ra = match kind_of_term c, ra with
+    | IsProd (_,_,c), Declarations.Mrec i :: ra' ->
 	(match kind_of_term c with
-	   | IsProd (_,_,c) -> true::(check_branch c ra')
-	   | _ ->
-	       error "Not a recursive eliminator: some induction hypothesis is lacking")
-    | IsLetIn (_,_,_,c), ra' -> false::(check_branch c ra)
-    | IsProd (_,_,c), _ :: ra -> false::(check_branch c ra)
+	   | IsProd (_,t,c) when is_indhyp (p+1) npred t ->
+	       true::(check_branch (p+2) c ra')
+	   | _ -> false::(check_branch (p+1) c ra'))
+    | IsLetIn (_,_,_,c), ra' -> false::(check_branch (p+1) c ra)
+    | IsProd (_,_,c), _ :: ra -> false::(check_branch (p+1) c ra)
     | _, [] -> []
     | _ ->
 	error"Not a recursive eliminator: some constructor argument is lacking"
@@ -1287,10 +1298,10 @@ let compute_elim_signature_and_roughly_check elimt mind =
   let rec check_elim c n =
     if n = nconstr then []
     else match kind_of_term c with
-    | IsProd (_,t,c) -> (check_branch t lra.(n)) :: (check_elim c (n+1))
+    | IsProd (_,t,c) -> (check_branch n t lra.(n)) :: (check_elim c (n+1))
     | _ -> error "Not an eliminator: some constructor case is lacking" in
-  let _,elimt2 = decompose_prod_n (mis_nparams mis + 1) elimt in
-  check_elim elimt2 0
+  let _,elimt3 = decompose_prod_n npred elimt2 in
+  check_elim elimt3 0
 
 let induction_from_context style hyp0 gl =
    (*test suivant sans doute inutile car protégé par le letin_tac avant appel*)