Add a syntax entry for fully applied constructor pattern

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

7 files changed, 18 insertions, 7 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fa92f9221c..91e374f59b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -158,6 +158,8 @@ let rec check_same_pattern p1 p2 =
         check_same_pattern a1 a2
     | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 ->
         List.iter2 check_same_pattern a1 a2
+    | CPatCstrExpl(_,c1,a1), CPatCstrExpl(_,c2,a2) when c1=c2 ->
+        List.iter2 check_same_pattern a1 a2
     | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
     | CPatPrim(_,i1), CPatPrim(_,i2) when i1=i2 -> ()
     | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
@@ -317,7 +319,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) =
 
 let mkPat loc qid l =
   (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
-  if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l)
+  if l = [] then CPatAtom (loc,Some qid) else CPatCstrExpl (loc,qid,l)
 
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
@@ -359,7 +361,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	  CPatRecord(loc, List.rev (ip projs args []))
 	with
 	  Not_found | No_match | Exit ->
-	    CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args) in
+	    CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), args) in
       insert_pat_alias loc p na
 
 and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 016f4a6584..7cca7347b7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1045,7 +1045,7 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
 	    | Some (_, head, pl) -> CPatCstr(loc, head, pl)
 	  in
 	intern_pat env aliases self_patt
-  | CPatCstr (loc, head, pl) ->
+  | CPatCstr (loc, head, pl) | CPatCstrExpl (loc, head, pl) ->
       let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl env in
       check_constructor_length genv loc c idslpl1 pl2;
       let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 0f95a94e8e..5ed7f31b19 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -830,6 +830,7 @@ type prim_token = Numeral of Bigint.bigint | String of string
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
+  | CPatCstrExpl of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_notation_substitution
@@ -940,6 +941,7 @@ let constr_loc = function
 let cases_pattern_expr_loc = function
   | CPatAlias (loc,_,_) -> loc
   | CPatCstr (loc,_,_) -> loc
+  | CPatCstrExpl (loc,_,_) -> loc
   | CPatAtom (loc,_) -> loc
   | CPatOr (loc,_) -> loc
   | CPatNotation (loc,_,_) -> loc
@@ -983,7 +985,7 @@ let rec cases_pattern_fold_names f a = function
   | CPatRecord (_, l) ->
       List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
   | CPatAlias (_,pat,id) -> f id a
-  | CPatCstr (_,_,patl) | CPatOr (_,patl) ->
+  | CPatCstr (_,_,patl) | CPatCstrExpl (_,_,patl) | CPatOr (_,patl) ->
       List.fold_left (cases_pattern_fold_names f) a patl
   | CPatNotation (_,_,(patl,patll)) ->
       List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 3bc3b06689..95c1af17d9 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -125,6 +125,7 @@ type prim_token = Numeral of Bigint.bigint | String of string
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
+  | CPatCstrExpl of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_notation_substitution
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index fa0e2fe52a..5d5f6e4d45 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -320,14 +320,17 @@ GEXTEND Gram
       [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ]
     | "99" RIGHTA [ ]
     | "10" LEFTA
+      [ p = pattern; "as"; id = ident ->
+	  CPatAlias (loc, p, id) ]
+    | "9" RIGHTA
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
           | _ -> Util.user_err_loc
               (cases_pattern_expr_loc p, "compound_pattern",
                Pp.str "Constructor expected."))
-      | p = pattern; "as"; id = ident ->
-	  CPatAlias (loc, p, id) ]
+      |"@"; r = Prim.reference; lp = LIST1 NEXT ->
+        CPatCstrExpl (loc, r, lp) ]
     | "1" LEFTA
       [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ]
     | "0"
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index c1466f9a02..811f170dc8 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -177,6 +177,9 @@ let rec pr_patt sep inh p =
   | CPatCstr (_,c,[]) -> pr_reference c, latom
   | CPatCstr (_,c,args) ->
       pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+  | CPatCstrExpl (_,c,args) ->
+      assert (args <> []);
+      str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
   | CPatAtom (_,None) -> str "_", latom
   | CPatAtom (_,Some r) -> pr_reference r, latom
   | CPatOr (_,pl) ->
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index a2b889fe03..64aa08ff2b 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -93,7 +93,7 @@ let rec add_vars_of_simple_pattern globs = function
 	(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
   | CPatDelimiters (_,_,p) ->
       add_vars_of_simple_pattern globs p
-  | CPatCstr (_,_,pl) ->
+  | CPatCstr (_,_,pl) | CPatCstrExpl (_,_,pl) ->
       List.fold_left add_vars_of_simple_pattern globs pl
   | CPatNotation(_,_,(pl,pll)) ->
       List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll))