Extension des parametres de Clear + Inst

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

3 files changed, 18 insertions, 11 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4bb01a6a41..e0a7e61ae7 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -42,9 +42,7 @@ GEXTEND Gram
     [ [ c = Prim.ast -> c ] ]
   ;
   constr:
-    [ [ c = constr8 -> c 
-      (*| IDENT "Context"; id = ident; IDENT "With"; c = constr8 ->
-        <:ast< (CONTEXT $id $c) >>*)
+    [ [ c = constr8 -> c
       | IDENT "Inst"; id = ident; "["; c = constr8; "]" ->
         <:ast< (CONTEXT $id $c) >>
       | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 142dac320c..42552fbd15 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -52,7 +52,7 @@ GEXTEND Gram
   ;
   idmeta_arg:
     [ [ id = Constr.ident -> id
-      | "?"; n = Prim.number -> <:ast< (METAID $n) >> ] ]
+      | "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >> ] ]
   ;
   qualidarg:
     [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >>
@@ -364,7 +364,7 @@ GEXTEND Gram
       |	IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr ->
         <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
       | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" ->
-        <:ast< (CONTEXT $id $c) >>
+        <:ast< (COMMAND (CONTEXT $id $c)) >>
       |	"'"; c = constrarg -> c ] ]
   ;
   simple_tactic:
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 =