Fixed commit 13125 (stricter check of induction args): an interpretation

checking function was used instead of a test of existence in the context.

Also restricted constr_of_id which had no reason to interpret a
posteriori an already interpreted identifier as a global
reference. Consequently adapted funind.

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

2 files changed, 19 insertions, 18 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7f1993079e..04ef9befb1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -136,9 +136,9 @@ let rec pr_value env = function
   | VList (a::_) ->
       str "a list (first element is " ++ pr_value env a ++ str")"
 
-(* Transforms an id into a constr if possible, or fails *)
+(* Transforms an id into a constr if possible, or fails with Not_found *)
 let constr_of_id env id =
-  construct_reference (Environ.named_context env) id
+  Term.mkVar (let _ = Environ.lookup_named id env in id)
 
 (* To embed tactics *)
 let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t),
@@ -1606,14 +1606,6 @@ 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
@@ -1623,19 +1615,31 @@ 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 ->
-	    sigma, ElimOnAnonHyp n
-	| VIntroPattern (IntroIdentifier id) ->
-	    interp_induction_ident ist gl sigma loc id
+	    ElimOnAnonHyp n
+	| VIntroPattern (IntroIdentifier id') ->
+	    if Tactics.is_quantified_hypothesis id' gl
+	    then ElimOnIdent (loc,id')
+	    else
+	      (try ElimOnConstr (constr_of_id env id',NoBindings)
+	       with Not_found ->
+		user_err_loc (loc,"",
+		pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
 	| VConstr ([],c) ->
-	    sigma, ElimOnConstr (c,NoBindings)
+	    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 ->
 	(* We were in non strict (interactive) mode *)
-	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 env sigma c in
+          sigma, ElimOnConstr (c,NoBindings)
 
 (* Associates variables with values and gives the remaining variables and
    values *)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 5fa9c220d4..9909b6d683 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -42,9 +42,6 @@ and interp_sign =
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
   Pretyping.ltac_var_map
 
-(** Transforms an id into a constr if possible *)
-val constr_of_id : Environ.env -> identifier -> constr
-
 (** To embed several objects in Coqast.t *)
 val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t
 val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr)