Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

1 files changed, 32 insertions, 2 deletions

diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 24c5ba5b..8e4b211f 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -346,8 +346,38 @@ let rec cases_pattern_of_glob_constr na = function
   | GHole (loc,_) -> PatVar (loc,na)
   | GRef (loc,ConstructRef cstr) ->
       PatCstr (loc,cstr,[],na)
-  | GApp (loc,GRef (_,ConstructRef cstr),l) ->
-      PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
+  | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
+      let mib,_ = Global.lookup_inductive ind in
+      let nparams = mib.Declarations.mind_nparams in
+      if nparams > List.length args then
+        user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
+      let params,args = list_chop nparams args in
+      List.iter (function GHole _ -> ()
+	| _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
+        params;
+      let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
+      PatCstr (loc,cstr,args,na)
+  | _ -> raise Not_found
+
+let rec cases_pattern_of_glob_constr na = function
+  | GVar (loc,id) when na<>Anonymous ->
+      (* Unable to manage the presence of both an alias and a variable *)
+      raise Not_found
+  | GVar (loc,id) -> PatVar (loc,Name id)
+  | GHole (loc,_) -> PatVar (loc,na)
+  | GRef (loc,ConstructRef cstr) ->
+      PatCstr (loc,cstr,[],na)
+  | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
+      let mib,_ = Global.lookup_inductive ind in
+      let nparams = mib.Declarations.mind_nparams in
+      if nparams > List.length args then
+        user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
+      let params,args = list_chop nparams args in
+      List.iter (function GHole _ -> ()
+	| _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
+        params;
+      let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
+      PatCstr (loc,cstr,args,na)
   | _ -> raise Not_found
 
 (* Turn a closed cases pattern into a glob_constr *)