Correction pour les variables abstraites dans les Tactic Definitions

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

1 files changed, 15 insertions, 5 deletions

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index ec7082984..e2f609072 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -67,13 +67,23 @@ let rec constr_list goalopt = function
     | None -> constr_list goalopt tl
     | Some goal ->
       let hyps = pf_hyps goal in
-      (try
+      if mem_named_context id hyps then
+        (id_of_string str,mkVar id)::(constr_list goalopt tl)
+      else
+        (try
+           let csr = Declare.global_reference CCI id in
+           (match kind_of_term csr with
+           | IsVar _ -> constr_list goalopt tl
+  	   | _ -> (id_of_string str,csr)::(constr_list goalopt tl))
+         with
+	 | Not_found -> (constr_list goalopt tl)))
+
+(*      (try
          let csr = Declare.global_reference CCI id in
          (match kind_of_term csr with
          | IsVar idc ->
            if mem_named_context idc hyps then
-             (id_of_string str,Declare.global_reference CCI id)::
-               (constr_list goalopt tl)
+             (id_of_string str,csr)::(constr_list goalopt tl)
            else
              constr_list goalopt tl
 	 | _ ->
@@ -84,7 +94,7 @@ let rec constr_list goalopt = function
         if mem_named_context id (pf_hyps goal) then
           (id_of_string str,mkVar id)::(constr_list goalopt tl)
         else
-          constr_list goalopt tl))
+          constr_list goalopt tl))*)
   | _::tl -> constr_list goalopt tl
   | [] -> []
 
@@ -401,7 +411,7 @@ let get_debug () = !debug
 (* Interprets any expression *)
 let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
 
-(*  mSGNL [<print_ast ast>];*)
+(* mSGNL [<print_ast ast>]; *)
 (* mSGNL [<print_ast (Termast.ast_of_constr false (Pretty.assumptions_for_print []) c)>] *)
 
   let value_interp debug =