amelioration du comportement de induction (retour a la version V8.0)

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

1 files changed, 9 insertions, 3 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fa9c2ed23..6196c4ece 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1648,8 +1648,13 @@ let compute_elim_sig ?elimc elimt =
 	| hiname,Some _,hi -> error "cannot recognize an induction schema"
 	| hiname,None,hi -> 
 	    let hi_ind, hi_args = decompose_app hi in
-	    let hi_is_ind = (* hi est d'un type inductif *)
-	      match kind_of_term hi_ind with | Ind (mind,_)  -> true | _ -> false in
+	    let hi_is_ind = (* hi est d'un type globalisable *)
+	      match kind_of_term hi_ind with
+		| Ind (mind,_)  -> true 
+		| Var _ -> true 
+		| Const _ -> true 
+		| Construct _ -> true 
+		| _ -> false in
 	    let hi_args_enough = (* hi a le bon nbre d'arguments *)
 	      List.length hi_args = List.length params + !res.nargs -1 in
 	    (* FIXME: Ces deux tests ne sont pas suffisants. *)
@@ -1827,6 +1832,7 @@ let recolle_clenv scheme lid elimclause gl =
     elimclause
 
 
+
 (* Unification of the goal and the principle applied to meta variables:
    (elimc ?i ?j ?k...?l). This solves partly meta variables (and may
     produce new ones). Then refine with the resulting term with holes.
@@ -1858,7 +1864,7 @@ let induction_from_context_l isrec elim_info lid names gl =
     + (if scheme.indarg <> None then 1 else 0) in
   (* Number of given induction args must be exact. *)
   if List.length lid <> nargs_indarg_farg + scheme.nparams then 
-    error "not the right number of arguments given to induction scheme";  
+      error "not the right number of arguments given to induction scheme";  
   let env = pf_env gl in
   (* hyp0 is used for re-introducing hyps at the right place afterward.
      We chose the first element of the list of variables on which to