Diverses corrections

- gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev]
- suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des
  quotations de tactiques pour simuler les métas des constr - quitte à devoir
  utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics]
- utilisation de error en place d'un "print_string" d'échec dans fourier
- améliorations espérées vis à vis de quelques "bizarreries" dans la gestion
  des Meta [pretyping]



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

5 files changed, 13 insertions, 16 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0e7c92a6c..f5ea021d4 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -142,10 +142,7 @@ GEXTEND Gram
     [ [ "_" -> (loc, Anonymous) ] ]
   ;
   global:
-    [ [ r = Prim.reference -> r
-
-      (* This is used in quotations *)
-      | id = METAIDENT -> Ident (loc,id_of_string id) ] ]
+    [ [ r = Prim.reference -> r ] ]
   ;
   constr_pattern:
     [ [ c = constr -> c ] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index c0fd07c17..c541b5a7e 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -95,6 +95,8 @@ GEXTEND Gram
 	  TacArg (TacExternal (loc,com,req,la))
       | st = simple_tactic -> TacAtom (loc,st)
       | a = may_eval_arg -> TacArg(a)
+      | IDENT "constr"; ":"; id = METAIDENT ->
+          TacArg(MetaIdArg (loc,false,id))
       | IDENT "constr"; ":"; c = Constr.constr ->
           TacArg(ConstrMayEval(ConstrTerm c))
       | IDENT "ipattern"; ":"; ipat = simple_intropattern -> 
@@ -125,7 +127,7 @@ GEXTEND Gram
       | r = reference -> Reference r
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
       (* Unambigous entries: tolerated w/o "ltac:" modifier *)
-      | id = METAIDENT -> MetaIdArg (loc,id)
+      | id = METAIDENT -> MetaIdArg (loc,true,id)
       | "()" -> TacVoid ] ]
   ;
   may_eval_arg:
@@ -148,7 +150,7 @@ GEXTEND Gram
       | c = Constr.constr -> ConstrTerm c ] ]
   ;
   tactic_atom:
-    [ [ id = METAIDENT -> MetaIdArg (loc,id)
+    [ [ id = METAIDENT -> MetaIdArg (loc,true,id)
       | n = integer -> Integer n
       | "()" -> TacVoid ] ]
   ;
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 5d59a8489..b26f8c77e 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -383,7 +383,8 @@ let parse_after_dot bp c =
 let rec next_token = parser bp
   | [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
       comm_loc bp; push_char c; next_token s
-  | [< ''$'; len = ident_tail (store 0 '$') >] ep -> 
+  | [< ''$'; ' ('a'..'z' | 'A'..'Z' | '_' as c); 
+      len = ident_tail (store 0 c) >] ep -> 
       comment_stop bp;
       (("METAIDENT", get_buff len), (bp,ep))
   | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 55c6a4387..2a46388c3 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -957,7 +957,8 @@ let rec pr_tac inherited tac =
 and pr_tacarg = function
   | TacDynamic (loc,t) ->
       pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
-  | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
+  | MetaIdArg (loc,true,s) -> pr_with_comments loc (str ("$" ^ s))
+  | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s))
   | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e698a187c..6313a553e 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -470,19 +470,15 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       <:expr< Tacexpr.TacFun
         ($mlexpr_of_list mlexpr_of_ident_option idol$,
          $mlexpr_of_tactic body$) >>
-(*
-  | Tacexpr.TacFunRec of $dloc$ * identifier * tactic_fun_ast
-*)
-(*
-  | Tacexpr.TacArg (Tacexpr.AstTacArg (Coqast.Nmeta $dloc$ id)) -> anti loc id
-*)
-  | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,id)) -> anti loc id
+  | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,true,id)) -> anti loc id
   | Tacexpr.TacArg t ->
       <:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >>
   | _ -> failwith "Quotation of tactic expressions: TODO"
 
 and mlexpr_of_tactic_arg = function
-  | Tacexpr.MetaIdArg (loc,id) -> anti loc id
+  | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id
+  | Tacexpr.MetaIdArg (loc,false,id) -> 
+      <:expr< Tacexpr.ConstrMayEval (Rawterm.ConstrTerm $anti loc id$) >>
   | Tacexpr.TacCall (loc,t,tl) ->
       <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
   | Tacexpr.Tacexp t ->