Prise en compte des noms longs dans les Hints et les Coercions

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

3 files changed, 30 insertions, 21 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index 497a15f9d8..8bda3545ae 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -170,9 +170,7 @@ let rec coerce_to_var v = function
   | Node(_,"QUALID",[Nvar(_,id)]) -> id
   | ast -> user_err_loc
         (loc ast,"Ast.coerce_to_var",
-         [< 'sTR"the variable "; 'sTR v;
-            'sTR" was bound to"; 'bRK(1,1); print_ast ast; 'sPC;
-            'sTR"instead of a (list of) variable(s)." >])
+         [< 'sTR"This expression should be a simple identifier" >])
 
 let env_assoc_value loc v env =
   try 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 207c624974..c1b0c96604 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -130,7 +130,7 @@ GEXTEND Gram
 	  <:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Constructors"; c = identarg;  "." ->
+	IDENT "Constructors"; c = qualidarg;  "." ->
 	  <:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
@@ -138,15 +138,15 @@ GEXTEND Gram
 	  <:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames)) 
 		   $n $c (TACTIC $tac))>>
 	  
-      | IDENT "Hints"; IDENT "Resolve"; l = ne_identarg_list; 
+      | IDENT "Hints"; IDENT "Resolve"; l = ne_qualidarg_list; 
 	dbnames = opt_identarg_list; "." ->
           <:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
 	  
-      | IDENT "Hints"; IDENT "Immediate"; l = ne_identarg_list; 
+      | IDENT "Hints"; IDENT "Immediate"; l = ne_qualidarg_list; 
 	dbnames = opt_identarg_list; "." ->
           <:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
 	  
-      | IDENT "Hints"; IDENT "Unfold"; l = ne_identarg_list;
+      | IDENT "Hints"; IDENT "Unfold"; l = ne_qualidarg_list;
 	dbnames = opt_identarg_list; "." ->
           <:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
 	  
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c628c2baff..60b0cb5c12 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -309,6 +309,12 @@ GEXTEND Gram
 GEXTEND Gram
   GLOBAL: gallina_ext;
 
+  def_body:
+    [ [
+	c1 = Constr.constr; ":"; c2 = Constr.constr ->
+          <:ast< (CONSTR (CAST $c1 $c2)) >>
+      | c = Constr.constr -> <:ast< (CONSTR $c) >>
+  ] ];
   gallina_ext:
     [ [ 
 (* Sections *)
@@ -324,31 +330,36 @@ GEXTEND Gram
 	  <:ast< (OPAQUE ($LIST $l)) >>
 
 (* Coercions *)
-      | IDENT "Coercion"; s = identarg; ":="; c = Constr.constr; "." ->
-          <:ast< (DEFINITION "COERCION" $s (CONSTR $c)) >>
-      | IDENT "Coercion"; s = identarg; ":="; c1 = Constr.constr; ":";
+      (* BUG: "Coercion S.T := A." n'est pas reconnu comme une phrase, pq?? *)
+      | IDENT "Coercion"; qid = qualidarg; ":="; c = def_body; "." ->
+          let s = Ast.coerce_to_var "qid" qid in
+          <:ast< (DEFINITION "COERCION" ($VAR $s) $c) >>
+(*
+      | IDENT "Coercion"; qid = qualidarg; ":="; c1 = Constr.constr; ":";
          c2 = Constr.constr; "." ->
-          <:ast< (DEFINITION "COERCION" $s (CONSTR (CAST $c1 $c2))) >>
+          let s = Ast.coerce_to_var "qid" qid in
+          <:ast< (DEFINITION "COERCION" ($VAR $s) (CONSTR (CAST $c1 $c2))) >>
+*)
       | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
 	 c = constrarg; "." ->
           <:ast< (DEFINITION "LCOERCION" $s $c) >>
       | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
 	 c1 = Constr.constr; ":"; c2 = Constr.constr; "." ->
           <:ast< (DEFINITION "LCOERCION" $s (CONSTR (CAST $c1 $c2))) >>
-      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identarg;
-         ":"; c = identarg; ">->"; d = identarg; "." ->
+      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = qualidarg;
+         ":"; c = qualidarg; ">->"; d = qualidarg; "." ->
           <:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >>
-      | IDENT "Identity"; IDENT "Coercion"; f = identarg; ":";
-         c = identarg; ">->"; d = identarg; "." ->
+      | IDENT "Identity"; IDENT "Coercion"; f = qualidarg; ":";
+         c = qualidarg; ">->"; d = qualidarg; "." ->
           <:ast< (COERCION "" "IDENTITY" $f $c $d) >>
-      | IDENT "Coercion"; IDENT "Local"; f = identarg; ":"; c = identarg;
-        ">->"; d = identarg; "." ->
+      | IDENT "Coercion"; IDENT "Local"; f = qualidarg; ":"; c = qualidarg;
+        ">->"; d = qualidarg; "." ->
           <:ast< (COERCION "LOCAL" "" $f $c $d) >>
-      | IDENT "Coercion"; f = identarg; ":"; c = identarg; ">->";
-         d = identarg; "." -> <:ast< (COERCION "" "" $f $c $d) >>
-      | IDENT "Class"; IDENT "Local"; c = identarg; "." ->
+      | IDENT "Coercion"; f = qualidarg; ":"; c = qualidarg; ">->";
+         d = qualidarg; "." -> <:ast< (COERCION "" "" $f $c $d) >>
+      | IDENT "Class"; IDENT "Local"; c = qualidarg; "." ->
           <:ast< (CLASS "LOCAL" $c) >>
-      | IDENT "Class"; c = identarg; "." -> <:ast< (CLASS "" $c) >>
+      | IDENT "Class"; c = qualidarg; "." -> <:ast< (CLASS "" $c) >>
 
 (* Implicit *)
       | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = constrarg;