Extension des parametres de Clear + Inst

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

1 files changed, 15 insertions, 6 deletions

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 6b0078b4c1..4b45132455 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -78,6 +78,16 @@ let constr_of_Constr_context = function
     anomalylabstrm "constr_of_Constr_context" [<'sTR
       "Not a Constr_context tactic_arg">]
 
+(* Gives identifiers and makes the possible injection constr -> ident *)
+let make_ids ast = function
+  | Identifier id -> id
+  | Constr c ->
+    (try destVar c with
+    | Invalid_argument "destVar" ->
+      anomalylabstrm "make_ids"
+      [<'sTR "This term cannot be reduced to an identifier"; 'fNL; print_ast ast>])
+  | _ -> anomalylabstrm "make_ids" [< 'sTR "Not an identifier" >]
+
 (* Transforms a named_context into a (string * constr) list *)
 let make_hyps = List.map (fun (id,_,typ) -> (string_of_id id,body_of_type typ))
 
@@ -514,11 +524,11 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
        with | Not_found ->
          (try (vcontext_interp (evc,env,lfun,lmatch,goalopt,debug) (lookup s))
           with | Not_found -> VArg (Identifier (id_of_string s))))
-    | Node(loc,"METAID",[Num(_,n)]) ->
+(*    | Node(loc,"METAID",[Num(_,n)]) ->
       (try VArg (Identifier (destVar (List.assoc n lmatch))) with
        | Invalid_argument "destVar" ->
          user_err_loc (loc, "Tacinterp.val_interp",[<'sTR
-          "Metavariable "; 'iNT n; 'sTR " must be an identifier" >]))
+          "Metavariable "; 'iNT n; 'sTR " must be an identifier" >]))*)
     | Str(_,s) -> VArg (Quoted_string s)
     | Num(_,n) -> VArg (Integer n)
     | Node(_,"COMMAND",[c]) ->
@@ -534,7 +544,7 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
       VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug)
         (redname,args)))
     | Node(_,"CLAUSE",cl) ->
-      VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp
+      VArg (Clause (List.map (fun ast -> make_ids ast (unvarg (val_interp
         (evc,env,lfun,lmatch,goalopt,debug) ast))) cl))
     | Node(_,"TACTIC",[ast]) ->
       VArg (Tac ((tac_interp lfun lmatch debug ast),ast))
@@ -964,9 +974,8 @@ and com_interp (evc,env,lfun,lmatch,goalopt,debug) = function
       errorlabstrm "com_interp" [<'sTR "Unbound context identifier";
         print_ast ast>])
   | c ->
-      VArg (Constr
-	      (interp_constr_gen evc env (constr_list goalopt lfun) lmatch
-		 c None))
+    VArg (Constr
+      (interp_constr_gen evc env (constr_list goalopt lfun) lmatch c None))
 
 (* Interprets a CASTEDCOMMAND expression *)
 and cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) com =