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

9 files changed, 33 insertions, 28 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7b2b1ca28f..784283358a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,10 @@
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
 =========================================
 
+** Removal of Tacinterp.constr_of_id **
+
+Use instead either global_reference or construct_reference in constrintern.ml.
+
 ** Optimizing calls to Evd functions **
 
 Evars are split into defined evars and undefined evars; for
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bef89909de..361df3d1cf 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1009,7 +1009,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 	  | _ -> ()
 
       in
-      Tacinterp.constr_of_id (pf_env g) equation_lemma_id
+      Constrintern.construct_reference (pf_hyps g) equation_lemma_id
   in
   let nb_intro_to_do = nb_prod (pf_concl g) in
     tclTHEN
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b756492b51..5ac5f9ce84 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -283,7 +283,7 @@ let change_property_sort toSort princ princName =
      compose_prod args (mkSort toSort)
     )
   in
-  let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in
+  let princName_as_constr = Constrintern.global_reference princName in
   let init =
     let nargs =  (princ_info.nparams + (List.length  princ_info.predicates)) in
     mkApp(princName_as_constr,
@@ -688,7 +688,7 @@ let build_case_scheme fa =
   let env = Global.env ()
   and sigma = Evd.empty in
 (*   let id_to_constr id =  *)
-(*     Tacinterp.constr_of_id env  id *)
+(*     Constrintern.global_reference  id *)
 (*   in  *)
   let funs =  (fun (_,f,_) ->
 		 try Libnames.constr_of_global (Nametab.global f)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ccbabead3d..7ba1f71dc9 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -232,7 +232,7 @@ let derive_inversion fix_names =
   try
     (* we first transform the fix_names identifier into their corresponding constant *)
     let fix_names_as_constant =
-      List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names
+      List.map (fun id -> destConst (Constrintern.global_reference id)) fix_names
     in
     (*
        Then we check that the graphs have been defined
@@ -249,7 +249,7 @@ let derive_inversion fix_names =
 	  Ensures by : register_built
 	  i*)
 	(List.map
-	   (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id)))
+	   (fun id -> destInd (Constrintern.global_reference (mk_rel_id id)))
 	   fix_names
 	)
     with e ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 28de815ca0..080073cbc0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -84,7 +84,7 @@ let nf_zeta =
 (* [id_to_constr id] finds the term associated to [id] in the global environment *)
 let id_to_constr id =
   try
-    Tacinterp.constr_of_id (Global.env ())  id
+    Constrintern.global_reference id
   with Not_found ->
     raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id))
 
@@ -797,7 +797,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let finfo = find_Function_infos f_as_constant in
 	 update_Function
 	   {finfo with
-	      correctness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_correct_id f_id)))
+	      correctness_lemma = Some (destConst (Constrintern.global_reference (mk_correct_id f_id)))
 	   }
 
       )
@@ -849,7 +849,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let finfo = find_Function_infos f_as_constant in
 	 update_Function
 	   {finfo with
-	      completeness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_complete_id f_id)))
+	      completeness_lemma = Some (destConst (Constrintern.global_reference (mk_complete_id f_id)))
 	   }
       )
       funs;
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ccc37046f9..1cf74025ab 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -129,7 +129,7 @@ let prNamedRLDecl s lc =
   end
 
 let showind (id:identifier) =
-  let cstrid = Tacinterp.constr_of_id (Global.env()) id in
+  let cstrid = Constrintern.global_reference id in
   let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
   let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
   List.iter (fun (nm, optcstr, tp) ->
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 3c3a36f037..5d282a5cb2 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -1225,7 +1225,7 @@ let do_build_inductive
   let env =
     Array.fold_right
       (fun id env ->
-	 Environ.push_named (id,None,Typing.type_of env Evd.empty (Tacinterp.constr_of_id env id))  env
+	 Environ.push_named (id,None,Typing.type_of env Evd.empty (Constrintern.global_reference id))  env
       )
       funnames
       (Global.env ())
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)