L'application de ltac attend une référence; meilleure protection contre

les erreurs


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

3 files changed, 11 insertions, 16 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 859865ee45..a7c37160ac 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -207,7 +207,7 @@ GEXTEND Gram
 	  ConstrMayEval (ConstrContext (id,c))
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
-      | qid = lqualid -> qid
+      | qid = lqualid -> Reference qid
       | ta = tactic_arg0 -> ta ] ]
   ;
   tactic_arg1:
@@ -218,13 +218,13 @@ GEXTEND Gram
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
       | qid = lqualid; la = LIST1 tactic_arg0 -> TacCall (loc,qid,la)
-      | qid = lqualid -> qid
+      | qid = lqualid -> Reference qid
       | ta = tactic_arg0 -> ta ] ]
   ;
   tactic_arg0:
     [ [ "("; a = tactic_expr; ")" -> Tacexp a
       | "()" -> TacVoid
-      | qid = lqualid -> qid
+      | qid = lqualid -> Reference qid
       | n = Prim.integer -> Integer n
       | id = METAIDENT -> MetaIdArg (loc,id)
       |	"?" -> ConstrMayEval (ConstrTerm <:ast< (ISEVAR) >>)
@@ -232,11 +232,7 @@ GEXTEND Gram
       |	"'"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ]
   ;
   lqualid:
-    [ [ qid = Prim.reference -> 
-(*  match Nametab.repr_qualid qid with
-  | (dir,id) when dir = Nameops.empty_dirpath -> Identifier id
-  | _ -> Qualid *) Reference qid
-    ] ]
+    [ [ ref = Prim.reference -> ref ] ]
   ;
 
   (* Definitions for tactics *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 28e51dcd12..a448166e1c 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -558,25 +558,24 @@ and pr6 = function
 
   | TacArg c -> pr_tacarg c
 
+and pr_reference = function 
+  | RQualid (_,qid) -> pr_qualid qid
+  | RIdent (_,id) -> pr_id id
+
 and pr_tacarg0 = function
   | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
   | MetaNumArg (_,n) -> str ("?" ^ string_of_int n )
   | MetaIdArg (_,s) -> str ("$" ^ s)
   | TacVoid -> str "()"
-  | Reference (RQualid (_,qid)) -> pr_qualid qid
-  | Reference (RIdent (_,id)) -> pr_id id
+  | Reference r -> pr_reference r
   | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c
   | ConstrMayEval c -> pr_may_eval pr_constr c
   | Integer n -> int n
-(*
-  | Tac of
-      'c * (Coqast.t,qualid or_metanum, identifier or_metaid) gen_tactic_expr
-*)
   | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")"
 
 and pr_tacarg1 = function
   | TacCall (_,f,l) ->
-      hov 0 (pr_tacarg0 f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l)
+      hov 0 (pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l)
   | Tacexp t -> !pr_rawtac t
   | t -> pr_tacarg0 t
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 4126250710..8729dce067 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -489,7 +489,7 @@ and mlexpr_of_tactic_arg = function
       <:expr< Tacexpr.AstTacArg $mlexpr_of_ast t$ >>
 *)
   | Tacexpr.TacCall (loc,t,tl) ->
-      <:expr< Tacexpr.TacCall loc $mlexpr_of_tactic_arg t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
+      <:expr< Tacexpr.TacCall loc $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
   | Tacexpr.Tacexp t ->
       <:expr< Tacexpr.Tacexp $mlexpr_of_tactic t$ >>
   | Tacexpr.ConstrMayEval c ->