Made intros_until and onInductionArg a bit stricter and robust

The tolerance for overloading "id" as quantified hypothesis and as
declared variable is kept - because induction_arg entry is not
available to extended tactics, e.g. "discriminate", and these
extensions do not know a priori if a name is quantified or declared.

However, an upstream check is done to ensure that an induction
argument exists as term if not quantified so that the tactics do not
have to check this individually by themselves.

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

3 files changed, 36 insertions, 28 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 140ddf8f4..d41dda23b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -331,7 +331,9 @@ let projectAndApply thin id eqname names depids gls =
   substHypIfVariable
     (* If no immediate variable in the equation, try to decompose it *)
     (* and apply a trailer which again try to substitute *)
-    (fun id -> dEqThen false (deq_trailer id) (Some (ElimOnIdent (dummy_loc,id))))
+    (fun id ->
+      dEqThen false (deq_trailer id)
+	(Some (ElimOnConstr (mkVar id,NoBindings))))
     id
     gls
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a754d1265..2b050b7eb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1606,6 +1606,14 @@ let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
   let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
   sigma, (loc,cb)
 
+let interp_induction_ident ist gl sigma loc id =
+  if Tactics.is_quantified_hypothesis id gl then
+    sigma, ElimOnIdent (loc,id)
+  else
+    let c = (RVar (loc,id),Some (CRef (Ident (loc,id)))) in
+    let c = interp_constr ist (pf_env gl) sigma c in
+    sigma, ElimOnConstr (c,NoBindings)
+
 let interp_induction_arg ist gl sigma arg =
   let env = pf_env gl in
   match arg with
@@ -1615,21 +1623,19 @@ let interp_induction_arg ist gl sigma arg =
   | ElimOnAnonHyp n as x -> sigma, x
   | ElimOnIdent (loc,id) ->
       try
-	sigma,
         match List.assoc id ist.lfun with
-	| VInteger n -> ElimOnAnonHyp n
-	| VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id)
-	| VConstr ([],c) -> ElimOnConstr (c,NoBindings)
+	| VInteger n ->
+	    sigma, ElimOnAnonHyp n
+	| VIntroPattern (IntroIdentifier id) ->
+	    interp_induction_ident ist gl sigma loc id
+	| VConstr ([],c) ->
+	    sigma, ElimOnConstr (c,NoBindings)
 	| _ -> user_err_loc (loc,"",
 	      strbrk "Cannot coerce " ++ pr_id id ++
 	      strbrk " neither to a quantified hypothesis nor to a term.")
       with Not_found ->
-	(* Interactive mode *)
-	if Tactics.is_quantified_hypothesis id gl then
-          sigma, ElimOnIdent (loc,id)
-	else
-          let c = interp_constr ist env sigma (RVar (loc,id),Some (CRef (Ident (loc,id)))) in
-          sigma, ElimOnConstr (c,NoBindings)
+	(* We were in non strict (interactive) mode *)
+	interp_induction_ident ist gl sigma loc id
 
 (* Associates variables with values and gives the remaining variables and
    values *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59befa785..0be1e08fc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -563,8 +563,13 @@ let intros_until = intros_until_gen true
 let intros_until_n = intros_until_n_gen true
 let intros_until_n_wored = intros_until_n_gen false
 
+let tclCHECKVAR id gl = ignore (pf_get_hyp gl id); tclIDTAC gl
+
+let try_intros_until_id_check id =
+  tclORELSE (intros_until_id id) (tclCHECKVAR id)
+
 let try_intros_until tac = function
-  | NamedHyp id -> tclTHEN (tclTRY (intros_until_id id)) (tac id)
+  | NamedHyp id -> tclTHEN (try_intros_until_id_check id) (tac id)
   | AnonHyp n -> tclTHEN (intros_until_n n) (onLastHypId tac)
 
 let rec intros_move = function
@@ -582,16 +587,13 @@ let dependent_in_decl a (_,c,t) =
    or a term with bindings *)
 
 let onInductionArg tac = function
-  | ElimOnConstr (c,lbindc as cbl) ->
-      if isVar c & lbindc = NoBindings then
-	tclTHEN (tclTRY (intros_until_id (destVar c))) (tac cbl)
-      else
-	tac cbl
+  | ElimOnConstr cbl ->
+      tac cbl
   | ElimOnAnonHyp n ->
       tclTHEN (intros_until_n n) (onLastHyp (fun c -> tac (c,NoBindings)))
   | ElimOnIdent (_,id) ->
-      (*Identifier apart because id can be quantified in goal and not typable*)
-      tclTHEN (tclTRY (intros_until_id id)) (tac (mkVar id,NoBindings))
+      (* A quantified hypothesis *)
+      tclTHEN (try_intros_until_id_check id) (tac (mkVar id,NoBindings))
 
 (**************************)
 (*  Refinement tactics    *)
@@ -790,9 +792,10 @@ let elim_in_context with_evars c = function
 let elim with_evars (c,lbindc as cx) elim =
   match kind_of_term c with
     | Var id when lbindc = NoBindings ->
-	tclTHEN (tclTRY (intros_until_id id))
+	tclTHEN (try_intros_until_id_check id)
 	  (elim_in_context with_evars cx elim)
-    | _ -> elim_in_context with_evars cx elim
+    | _ ->
+	elim_in_context with_evars cx elim
 
 (* The simplest elimination tactic, with no substitutions at all. *)
 
@@ -853,8 +856,8 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl =
 let general_case_analysis with_evars (c,lbindc as cx) =
   match kind_of_term c with
     | Var id when lbindc = NoBindings ->
-	tclTHEN (tclTRY (intros_until_id id))
-	(general_case_analysis_in_context with_evars cx)
+	tclTHEN (try_intros_until_id_check id)
+	  (general_case_analysis_in_context with_evars cx)
     | _ ->
 	general_case_analysis_in_context with_evars cx
 
@@ -3177,11 +3180,8 @@ let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls)
 (* Induction tactics *)
 
 (* This was Induction before 6.3 (induction only in quantified premisses) *)
-let raw_induct s = tclTHEN (intros_until_id s) (onLastHyp simplest_elim)
-let raw_induct_nodep n = tclTHEN (intros_until_n n) (onLastHyp simplest_elim)
-
-let simple_induct_id hyp = raw_induct hyp
-let simple_induct_nodep = raw_induct_nodep
+let simple_induct_id s = tclTHEN (intros_until_id s) (onLastHyp simplest_elim)
+let simple_induct_nodep n = tclTHEN (intros_until_n n) (onLastHyp simplest_elim)
 
 let simple_induct = function
   | NamedHyp id -> simple_induct_id id