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

4 files changed, 9 insertions, 4 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