bugs avec Pose et Assert

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

6 files changed, 28 insertions, 26 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e05ed48c5b..f529bf26cc 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -291,9 +291,9 @@ GEXTEND Gram
 	  TacMutualCofix (id,fd)
 
       | IDENT "Cut"; c = constr -> TacCut c
-      | IDENT "Assert"; c = constr -> TacTrueCut (None,c)
+      | IDENT "Assert"; c = constr -> TacTrueCut (Names.Anonymous,c)
       | IDENT "Assert"; c = constr; ":"; t = constr ->
-          TacTrueCut (Some (snd(coerce_to_id c)),t)
+          TacTrueCut (Names.Name (snd(coerce_to_id c)),t)
       | IDENT "Assert"; c = constr; ":="; b = constr ->
           TacForward (false,Names.Name (snd (coerce_to_id c)),b)
       | IDENT "Pose"; c = constr; ":="; b = constr ->
@@ -301,8 +301,8 @@ GEXTEND Gram
       | IDENT "Pose"; b = constr -> TacForward (true,Names.Anonymous,b)
       | IDENT "Generalize"; lc = LIST1 constr -> TacGeneralize lc
       | IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c
-      | IDENT "LetTac"; id = base_ident; ":="; c = constr; p = clause_pattern
-        -> TacLetTac (id,c,p)
+      | IDENT "LetTac"; (_,na) = name; ":="; c = constr; p = clause_pattern
+        -> TacLetTac (na,c,p)
       | IDENT "Instantiate"; n = natural; c = constr; cls = clause -> 
 	    TacInstantiate (n,c,cls)
       | IDENT "Specialize"; n = OPT natural; lcb = constr_with_bindings ->
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index ccac2ae731..b108ab4b42 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -55,7 +55,7 @@ let test_lpar_idnum_coloneq =
 
 (* idem for (x:t) *)
 let lpar_id_colon =
-  Gram.Entry.of_parser "test_lpar_id_colon"
+  Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       match Stream.npeek 1 strm with
         | [("","(")] ->
@@ -333,18 +333,20 @@ GEXTEND Gram
 
       | IDENT "cut"; c = constr -> TacCut c
       | IDENT "assert"; id = lpar_id_colon; t = lconstr; ")" ->
-          TacTrueCut (Some id,t)
+          TacTrueCut (Names.Name id,t)
       | IDENT "assert"; id = lpar_id_coloneq; b = lconstr; ")" ->
           TacForward (false,Names.Name id,b)
-      | IDENT "assert"; c = constr -> TacTrueCut (None,c)
+      | IDENT "assert"; c = constr -> TacTrueCut (Names.Anonymous,c)
       | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
 	  TacForward (true,Names.Name id,b)
       | IDENT "pose"; b = constr -> TacForward (true,Names.Anonymous,b)
       | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
       | IDENT "generalize"; IDENT "dependent"; c = constr ->
           TacGeneralizeDep c
-      | IDENT "set"; "("; id = base_ident; ":="; c = lconstr; ")";
-          p = clause -> TacLetTac (id,c,p)
+      | IDENT "set"; id = lpar_id_coloneq; c = lconstr; ")";
+          p = clause -> TacLetTac (Names.Name id,c,p)
+      | IDENT "set"; c = constr; p = clause ->
+          TacLetTac (Names.Anonymous,c,p)
       | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")";
 	  cls = clause ->
             TacInstantiate (n,c,cls)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index fe8b462d8c..b1e6cda093 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -271,12 +271,12 @@ GEXTEND Gram
     [ [ l = LIST1 onecorec SEP "with" -> l ] ]
   ;
   record_field:
-    [ [ id = identref; oc = of_type_with_opt_coercion; t = constr ->
+    [ [ id = name; oc = of_type_with_opt_coercion; t = constr ->
           (oc,AssumExpr (id,t))
-      | id = identref; oc = of_type_with_opt_coercion; t = constr;
+      | id = name; oc = of_type_with_opt_coercion; t = constr;
 	":="; b = constr ->
 	  (oc,DefExpr (id,b,Some t))
-      | id = identref; ":="; b = constr ->
+      | id = name; ":="; b = constr ->
 	  (false,DefExpr (id,b,None)) ] ]
   ;
   fields:
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 5599f58800..8142303043 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -266,12 +266,12 @@ GEXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
-    [ [ id = identref -> (false,AssumExpr(id,CHole loc))
-      | id = identref; oc = of_type_with_opt_coercion; t = lconstr ->
+    [ [ id = name -> (false,AssumExpr(id,CHole loc))
+      | id = name; oc = of_type_with_opt_coercion; t = lconstr ->
          (oc,AssumExpr (id,t))
-      | id = identref; oc = of_type_with_opt_coercion;
+      | id = name; oc = of_type_with_opt_coercion;
              t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t))
-      | id = identref; ":="; b = lconstr ->
+      | id = name; ":="; b = lconstr ->
          match b with
              CCast(_,b,t) -> (false,DefExpr(id,b,Some t))
            | _ -> (false,DefExpr(id,b,None)) ] ]
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 980bc63c23..3a6cfab0e6 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -472,9 +472,9 @@ and pr_atom1 = function
           prlist (fun (id,c) -> spc () ++ pr_id id ++ pr_arg pr_constr c)
 	  l))
   | TacCut c -> hov 1 (str "Cut" ++ pr_arg pr_constr c)
-  | TacTrueCut (None,c) -> 
+  | TacTrueCut (Anonymous,c) -> 
       hov 1 (str "Assert" ++ pr_arg pr_constr c)
-  | TacTrueCut (Some id,c) -> 
+  | TacTrueCut (Name id,c) -> 
       hov 1 (str "Assert" ++ spc () ++ pr_id id ++ str ":" ++ pr_constr c)
   | TacForward (false,na,c) ->
       hov 1 (str "Assert" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
@@ -485,11 +485,11 @@ and pr_atom1 = function
   | TacGeneralizeDep c ->
       hov 1 (str "Generalize" ++ spc () ++ str "Dependent" ++ spc () ++
       pr_constr c)
-  | TacLetTac (id,c,cl) ->
+  | TacLetTac (na,c,cl) ->
       let pcl = match cl with
           {onhyps=None;onconcl=true;concl_occs=[]} -> mt()
         | _ -> pr_clauses pr_ident cl in
-      hov 1 (str "LetTac" ++ spc () ++ pr_id id ++ str ":=" ++
+      hov 1 (str "LetTac" ++ spc () ++ pr_name na ++ str ":=" ++
              pr_constr c ++ pcl)
   | TacInstantiate (n,c,cls) ->
       hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++ 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e4f90ffa81..8df84e5736 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -374,19 +374,19 @@ let rec mlexpr_of_atomic_tactic = function
 
   | Tacexpr.TacCut c ->
       <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
-  | Tacexpr.TacTrueCut (ido,c) ->
-      let ido = mlexpr_of_ident_option ido in
-      <:expr< Tacexpr.TacTrueCut $ido$ $mlexpr_of_constr c$ >>
+  | Tacexpr.TacTrueCut (na,c) ->
+      let na = mlexpr_of_name na in
+      <:expr< Tacexpr.TacTrueCut $na$ $mlexpr_of_constr c$ >>
   | Tacexpr.TacForward (b,na,c) ->
       <:expr< Tacexpr.TacForward $mlexpr_of_bool b$ $mlexpr_of_name na$ $mlexpr_of_constr c$ >>
   | Tacexpr.TacGeneralize cl ->
       <:expr< Tacexpr.TacGeneralize $mlexpr_of_list mlexpr_of_constr cl$ >>
   | Tacexpr.TacGeneralizeDep c ->
       <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >>
-  | Tacexpr.TacLetTac (id,c,cl) ->
-      let id = mlexpr_of_ident id in
+  | Tacexpr.TacLetTac (na,c,cl) ->
+      let na = mlexpr_of_name na in
       let cl = mlexpr_of_clause_pattern cl in
-      <:expr< Tacexpr.TacLetTac $id$ $mlexpr_of_constr c$ $cl$ >>
+      <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ >>
 
   (* Derived basic tactics *)
   | Tacexpr.TacSimpleInduction (h,_) ->