Parameters in pattern first step.

In interp/constrintern.ml, '_' for constructor parameter are required if you use
AppExpl ('@Constr') and added in order to be erased at the last time if you do not
use '@'.

It makes the use of notation in pattern more permissive. For example,
-8<------
Inductive I (A: Type) : Type := C : A -> I A.

Notation "x <: T" := (C T x) (at level 38).

Definition uncast A (x : I A) :=
match x with
 | x <: _ => x
end.
-8<------
was forbidden.

Backward compatibility is strictly preserved expect for syntactic definitions:
While defining "Notation SOME = @Some", SOME had a special treatment and used to
be an alias of Some in pattern. It is now uniformly an alias of @Some ('_' must be
provided for parameters).

In interp/constrextern.ml, except if all the parameters are implicit and all the
arguments explicit (This covers all the cases of the test-suite), pattern are
generated with AppExpl (id est '@') (so with '_' for parameters) in order to
become compatible in any case with future behavior.

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

4 files changed, 190 insertions, 164 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 193b38ddb2..c0d597d2f1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -321,99 +321,110 @@ 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)
 
+let add_patt_for_params (ind,k) l =
+    Util.list_addn (Inductiveops.inductive_nparams ind) (CPatAtom (dummy_loc,None)) l
+
+let pattern_printable_in_both_syntax (ind,_ as c) =
+  let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
+  let nb_params = Inductiveops.inductive_nparams ind in
+  List.exists (fun (_,impls) ->
+    (List.length impls >= nb_params) &&
+      let params,args = Util.list_chop nb_params impls in
+      (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
+  ) impl_st
+
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try
     if !Flags.raw_print or !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
     match availability_of_prim_token p sc scopes with
-    | None -> raise No_match
-    | Some key ->
-      let loc = cases_pattern_loc pat in
-      insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
-  with No_match ->
-  try
-    if !Flags.raw_print or !print_no_symbol then raise No_match;
-    extern_symbol_pattern scopes vars pat
-      (uninterp_cases_pattern_notations pat)
+      | None -> raise No_match
+      | Some key ->
+	let loc = cases_pattern_loc pat in
+	insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
   with No_match ->
-  match pat with
-  | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
-  | PatVar (loc,Anonymous) -> CPatAtom (loc, None)
-  | PatCstr(loc,cstrsp,args,na) ->
-      let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-      let p =
-	try
-          if !Flags.raw_print then raise Exit;
-	  let projs = Recordops.lookup_projections (fst cstrsp) in
-	  let rec ip projs args acc =
-	    match projs with
-	      | [] -> acc
-	      | None :: q -> ip q args acc
-	      | Some c :: q ->
-		  match args with
-		    | [] -> raise No_match
-		    | CPatAtom(_, None) :: tail -> ip q tail acc
-			(* we don't want to have 'x = _' in our patterns *)
-		    | head :: tail -> ip q tail
+    try
+      if !Flags.raw_print or !print_no_symbol then raise No_match;
+      extern_symbol_pattern scopes vars pat
+	(uninterp_cases_pattern_notations pat)
+    with No_match ->
+      match pat with
+	| PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
+	| PatVar (loc,Anonymous) -> CPatAtom (loc, None)
+	| PatCstr(loc,cstrsp,args,na) ->
+	  let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+	  let p =
+	    try
+              if !Flags.raw_print then raise Exit;
+	      let projs = Recordops.lookup_projections (fst cstrsp) in
+	      let rec ip projs args acc =
+		match projs with
+		  | [] -> acc
+		  | None :: q -> ip q args acc
+		  | Some c :: q ->
+		    match args with
+		      | [] -> raise No_match
+		      | CPatAtom(_, None) :: tail -> ip q tail acc
+		    (* we don't want to have 'x = _' in our patterns *)
+		      | head :: tail -> ip q tail
 		        ((extern_reference loc Idset.empty (ConstRef c), head) :: acc)
-	    in
-	  CPatRecord(loc, List.rev (ip projs args []))
-	with
-	  Not_found | No_match | Exit ->
-	    CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args) in
-      insert_pat_alias loc p na
+	      in
+	      CPatRecord(loc, List.rev (ip projs args []))
+	    with
+		Not_found | No_match | Exit ->
+		  if pattern_printable_in_both_syntax cstrsp
+		  then CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args)
+		  else CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), add_patt_for_params cstrsp args) in
+	  insert_pat_alias loc p na
 
 and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
       match t,n with
-      | PatCstr (loc,(ind,_),l,na), n when n = Some 0 or n = None or 
-	 n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams ->
-        (* Abbreviation for the constructor name only *)
-	(match keyrule with
-        | NotationRule (sc,ntn) -> raise No_match
-        | SynDefRule kn ->
-	    let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
-	    let l = List.map (extern_cases_pattern_in_scope allscopes vars) l in
-	    insert_pat_alias loc (mkPat loc qid l) na)
-      | PatCstr (_,f,l,_), Some n when List.length l > n ->
-	  raise No_match
-      | PatCstr (loc,_,_,na),_ ->
-	(* Try matching ... *)
-	let subst,substlist = match_aconstr_cases_pattern t pat in
-	(* Try availability of interpretation ... *)
-	let p = match keyrule with
-          | NotationRule (sc,ntn) ->
-	      (match availability_of_notation (sc,ntn) allscopes with
-                  (* Uninterpretation is not allowed in current context *)
-              | None -> raise No_match
-                  (* Uninterpretation is allowed in current context *)
-	      | Some (scopt,key) ->
-	          let scopes' = Option.List.cons scopt scopes in
-	          let l =
-		    List.map (fun (c,(scopt,scl)) ->
-		      extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
-                      subst in
-		  let ll =
-		    List.map (fun (c,(scopt,scl)) ->
-		      let subscope = (scopt,scl@scopes') in
-		      List.map (extern_cases_pattern_in_scope subscope vars) c)
-                      substlist in
-		  insert_pat_delimiters loc
-		    (make_pat_notation loc ntn (l,ll)) key)
-          | SynDefRule kn ->
+	| PatCstr (loc,_,_,na),_ ->
+	  (* Try matching ... *)
+	  let (subst,substlist),more_args = match_aconstr_cases_pattern t pat in
+	  (* Try availability of interpretation ... *)
+	  let p = match keyrule with
+            | NotationRule (sc,ntn) ->
+	      begin match more_args with
+		|_::_ ->
+		  (* Parser and Constrintern do not understand a notation for
+		     partially applied constructor. *)
+		  raise No_match
+		|[] ->
+		  match availability_of_notation (sc,ntn) allscopes with
+		    (* Uninterpretation is not allowed in current context *)
+		    | None -> raise No_match
+		    (* Uninterpretation is allowed in current context *)
+		    | Some (scopt,key) ->
+	              let scopes' = Option.List.cons scopt scopes in
+	              let l =
+			List.map (fun (c,(scopt,scl)) ->
+			  extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
+			  subst in
+		      let ll =
+			List.map (fun (c,(scopt,scl)) ->
+			  let subscope = (scopt,scl@scopes') in
+			  List.map (extern_cases_pattern_in_scope subscope vars) c)
+			  substlist in
+		      insert_pat_delimiters loc
+			(make_pat_notation loc ntn (l,ll)) key
+	      end
+            | SynDefRule kn ->
 	      let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
-	      let l =
-		List.map (fun (c,(scopt,scl)) ->
-                  extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) 
+	      let l1 =
+		List.rev_map (fun (c,(scopt,scl)) ->
+                  extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
                   subst in
+	      let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
               assert (substlist = []);
-	      mkPat loc qid l in
-	insert_pat_alias loc p na
-      | PatVar (loc,Anonymous),_ -> CPatAtom (loc, None)
-      | PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id)))
+	      mkPat loc qid (List.rev_append l1 l2) in
+	  insert_pat_alias loc p na
+	| PatVar (loc,Anonymous),_ -> CPatAtom (loc, None)
+	| PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id)))
     with
 	No_match -> extern_symbol_pattern allscopes vars t rules
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3d39f0f928..0f5d66282f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -157,10 +157,10 @@ let error_bad_inductive_type loc =
   user_err_loc (loc,"",str
     "This should be an inductive type applied to names or \"_\".")
 
-let error_inductive_parameter_not_implicit loc =
+let error_parameter_not_implicit loc =
   user_err_loc (loc,"", str
-   ("The parameters of inductive types do not bind in\n"^
-    "the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
+   "The parameters do not bind in patterns;" ++ spc () ++ str
+    "they must be replaced by '_'.")
 
 (**********************************************************************)
 (* Pre-computing the implicit arguments and arguments scopes needed   *)
@@ -740,10 +740,8 @@ let rec simple_adjust_scopes n scopes =
   | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
 
 let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
-  let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
-  let npar = mib.Declarations.mind_nparams in
-  snd (list_chop (npar + List.length pl1)
-    (simple_adjust_scopes (npar + List.length pl1 + List.length pl2)
+  snd (list_chop (List.length pl1)
+    (simple_adjust_scopes (List.length pl1 + List.length pl2)
       (find_arguments_scope (ConstructRef cstr))))
 
 (**********************************************************************)
@@ -789,12 +787,15 @@ let check_or_pat_variables loc ids idsl =
     user_err_loc (loc, "", str
     "The components of this disjunctive pattern must bind the same variables.")
 
-let check_constructor_length env loc cstr pl pl0 =
+(** @param with_params says if _ for params were asked to the user.
+    @return if letin are included *)
+let check_constructor_length env loc cstr with_params pl pl0 =
+  let nargs = Inductiveops.mis_constructor_nargs cstr in
   let n = List.length pl + List.length pl0 in
-  let nargs = Inductiveops.constructor_nrealargs env cstr in
-  let nhyps = Inductiveops.constructor_nrealhyps env cstr in
-  if n <> nargs && n <> nhyps (* i.e. with let's *) then
-    error_wrong_numarg_constructor_loc loc env cstr nargs
+  if n = nargs then false else
+    (n = (fst (Inductiveops.inductive_nargs (fst cstr))) + Inductiveops.constructor_nrealhyps cstr) ||
+      (error_wrong_numarg_constructor_loc loc env cstr
+	 (if with_params then nargs else nargs - (Inductiveops.inductive_nparams (fst cstr))))
 
 (* Manage multiple aliases *)
 
@@ -816,18 +817,6 @@ let message_redundant_alias (id1,id2) =
 let error_invalid_pattern_notation loc =
   user_err_loc (loc,"",str "Invalid notation for pattern.")
 
-let chop_aconstr_constructor loc (ind,k) args =
-  if List.length args = 0 then (* Tolerance for a @id notation *) args else
-    begin
-      let mib,_ = Global.lookup_inductive ind in
-      let nparams = mib.Declarations.mind_nparams in
-      if nparams > List.length args then error_invalid_pattern_notation loc;
-      let params,args = list_chop nparams args in
-      List.iter (function AHole _ -> ()
-	| _ -> error_invalid_pattern_notation loc) params;
-      args
-    end
-
 let rec subst_pat_iterator y t (subst,p) = match p with
   | PatVar (_,id) as x ->
       if id = Name y then t else [subst,x]
@@ -836,6 +825,18 @@ let rec subst_pat_iterator y t (subst,p) = match p with
       let pl = simple_product_of_cases_patterns l' in
       List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl
 
+(** @raise NotEnoughArguments only in the case of [subst_cases_pattern] thanks to
+    preconditions in other cases. *)
+let chop_params_pattern loc (ind,_) args with_letin =
+  let nparams = if with_letin
+    then fst (Inductiveops.inductive_nargs ind)
+    else Inductiveops.inductive_nparams ind in
+  if nparams > List.length args then error_not_enough_arguments loc;
+  let params,args = list_chop nparams args in
+  List.iter (function PatVar(_,Anonymous) -> ()
+    | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit loc') params;
+  args
+
 let subst_cases_pattern loc alias intern fullsubst env a =
   let rec aux alias (subst,substlist as fullsubst) = function
   | AVar id ->
@@ -859,11 +860,10 @@ let subst_cases_pattern loc alias intern fullsubst env a =
   | ARef (ConstructRef c) ->
       ([],[[], PatCstr (loc,c, [], alias)])
   | AApp (ARef (ConstructRef cstr),args) ->
-      let args = chop_aconstr_constructor loc cstr args in
       let idslpll = List.map (aux Anonymous fullsubst) args in
       let ids',pll = product_of_cases_patterns [] idslpll in
       let pl' = List.map (fun (asubst,pl) ->
-        asubst,PatCstr (loc,cstr,pl,alias)) pll in
+        asubst,PatCstr (loc,cstr,chop_params_pattern loc cstr pl false,alias)) pll in
 	ids', pl'
   | AList (x,_,iter,terminator,lassoc) ->
       (try
@@ -890,36 +890,41 @@ type pattern_qualid_kind =
       ((identifier * identifier) list * cases_pattern) list) list
   | VarPat of identifier
 
-let find_constructor ref f aliases pats env =
+let find_constructor add_params ref f aliases pats env =
+  let add_params (ind,_ as c) = match add_params with
+    |Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c
+      then fst (Inductiveops.inductive_nargs ind)
+      else Inductiveops.inductive_nparams ind in
+      Util.list_make nb ([],[([],PatVar(dummy_loc,Anonymous))])
+    |None -> [] in
   let (loc,qid) = qualid_of_reference ref in
   let gref =
     try locate_extended qid
     with Not_found -> raise (InternalizationError (loc,NotAConstructor ref)) in
   match gref with
-  | SynDef sp ->
+    | SynDef sp ->
       let (vars,a) = Syntax_def.search_syntactic_definition sp in
       (match a with
-       | ARef (ConstructRef cstr) ->
-	   assert (vars=[]);
-	   cstr, [], pats
-       | AApp (ARef (ConstructRef cstr),args) ->
-	   let args = chop_aconstr_constructor loc cstr args in
-	   let nvars = List.length vars in
-	   if List.length pats < nvars then error_not_enough_arguments loc;
-	   let pats1,pats2 = list_chop nvars pats in
-	   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
-	   let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) env) args in
-	   cstr, idspl1, pats2
-       | _ -> raise Not_found)
-
-  | TrueGlobal r ->
+	| ARef (ConstructRef cstr) ->
+	  assert (vars=[]);
+	  cstr,add_params cstr, pats
+	| AApp (ARef (ConstructRef cstr),args) ->
+	  let nvars = List.length vars in
+	  if List.length pats < nvars then error_not_enough_arguments loc;
+	  let pats1,pats2 = list_chop nvars pats in
+	  let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
+	  let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) env) args in
+	  cstr, idspl1, pats2
+	| _ -> raise Not_found)
+
+    | TrueGlobal r ->
       let rec unf = function
         | ConstRef cst ->
-	    let v = Environ.constant_value (Global.env()) cst in
-	    unf (global_of_constr v)
+	  let v = Environ.constant_value (Global.env()) cst in
+	  unf (global_of_constr v)
         | ConstructRef cstr ->
-	    Dumpglob.add_glob loc r;
-	    cstr, [], pats
+	  Dumpglob.add_glob loc r;
+	  cstr, add_params cstr, pats
         | _ -> raise Not_found
       in unf r
 
@@ -929,20 +934,20 @@ let find_pattern_variable = function
 
 let maybe_constructor ref f aliases env =
   try
-    let c,idspl1,pl2 = find_constructor ref f aliases [] env in
+    let c,idspl1,pl2 = find_constructor (Some 0) ref f aliases [] env in
     assert (pl2 = []);
     ConstrPat (c,idspl1)
   with
-      (* patt var does not exists globally *)
+    (* patt var does not exists globally *)
     | InternalizationError _ -> VarPat (find_pattern_variable ref)
-      (* patt var also exists globally but does not satisfy preconditions *)
+    (* patt var also exists globally but does not satisfy preconditions *)
     | (Environ.NotEvaluableConst _ | Not_found) ->
-        if_warn msg_warning (str "pattern " ++ pr_reference ref ++
-              str " is understood as a pattern variable");
-        VarPat (find_pattern_variable ref)
+      if_warn msg_warning (str "pattern " ++ pr_reference ref ++
+			     str " is understood as a pattern variable");
+      VarPat (find_pattern_variable ref)
 
-let mustbe_constructor loc ref f aliases patl env =
-  try find_constructor ref f aliases patl env
+let mustbe_constructor loc add_params ref f aliases patl env =
+  try find_constructor add_params ref f aliases patl env
   with (Environ.NotEvaluableConst _ | Not_found) ->
     raise (InternalizationError (loc,NotAConstructor ref))
 
@@ -1037,6 +1042,13 @@ let sort_fields mode loc l completer =
 
 let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
   let intern_pat = intern_cases_pattern genv in
+  let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
+    let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
+    let idslpl2 = List.map2 (fun x -> intern_pat {env with tmp_scope = x} ([],[])) argscs2 pl2 in
+    let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
+    let pl' = List.map (fun (asubst,pl) ->
+      (asubst, PatCstr (loc,c,chop_params_pattern loc c pl with_letin,alias_of aliases))) pll in
+    ids',pl' in
   match pat with
   | CPatAlias (loc, p, id) ->
       let aliases' = merge_aliases aliases id in
@@ -1049,15 +1061,14 @@ 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) | 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
-      let idslpl2 = List.map2 (fun x -> intern_pat {env with tmp_scope = x} ([],[])) argscs2 pl2 in
-      let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
-      let pl' = List.map (fun (asubst,pl) ->
-        (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in
-      ids',pl'
+  | CPatCstr (loc, head, pl) ->
+      let c,idslpl1,pl2 = mustbe_constructor loc (Some (List.length pl)) head intern_pat aliases pl env in
+      let with_letin = check_constructor_length genv loc c false idslpl1 pl2 in
+      intern_cstr_with_all_args loc c with_letin idslpl1 pl2
+  | CPatCstrExpl (loc, head, pl) ->
+      let c,idslpl1,pl2 = mustbe_constructor loc None head intern_pat aliases pl env in
+      let with_letin = check_constructor_length genv loc c true idslpl1 pl2 in
+      intern_cstr_with_all_args loc c with_letin idslpl1 pl2
   | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]))
       when Bigint.is_strictly_pos p ->
       intern_pat env aliases (CPatPrim(loc,Numeral(Bigint.neg p)))
@@ -1085,10 +1096,8 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
   | CPatAtom (loc, Some head) ->
       (match maybe_constructor head intern_pat aliases env with
 	 | ConstrPat (c,idspl) ->
-	     check_constructor_length genv loc c idspl [];
-	     let (ids',pll) = product_of_cases_patterns ids idspl in
-	     (ids,List.map (fun (asubst,pl) ->
-	       (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll)
+	   let with_letin = check_constructor_length genv loc c false idspl [] in
+	   intern_cstr_with_all_args loc c with_letin idspl []
 	 | VarPat id ->
 	     let ids,asubst = merge_aliases aliases id in
 	     (ids,[asubst, PatVar (loc,alias_of (ids,asubst))]))
@@ -1399,7 +1408,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	    | GRef (loc,IndRef ind) -> (loc,ind,[])
 	    | GApp (loc,GRef (_,IndRef ind),l) -> (loc,ind,l)
 	    | _ -> error_bad_inductive_type (loc_of_glob_constr t) in
-	let nparams, nrealargs = inductive_nargs globalenv ind in
+	let nparams, nrealargs = inductive_nargs_env globalenv ind in
 	let nindargs = nparams + nrealargs in
 	if List.length l <> nindargs then
 	  error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
@@ -1409,7 +1418,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	  | c -> user_err_loc (loc_of_glob_constr c,"",str "Not a name.")) l in
 	let parnal,realnal = list_chop nparams nal in
 	if List.exists (fun (_,na) -> na <> Anonymous) parnal then
-	  error_inductive_parameter_not_implicit loc;
+	  error_parameter_not_implicit loc;
 	realnal, Some (loc,ind,nparams,List.map snd realnal)
     | None ->
 	[], None in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index b484d175b6..ab85f84651 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -782,6 +782,10 @@ let match_aconstr u c (metas,pat) =
     metas ([],[],[])
 
 (* Matching cases pattern *)
+let add_patterns_for_params (ind,k) l =
+  let mib,_ = Global.lookup_inductive ind in
+  let nparams = mib.Declarations.mind_nparams in
+    Util.list_addn nparams (PatVar (dummy_loc,Anonymous)) l
 
 let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
   try
@@ -791,39 +795,41 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::sigma,sigmalist,x
 
-let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
-  | r1, AVar id2 when List.mem id2 metas -> bind_env_cases_pattern sigma id2 r1
-  | PatVar (_,Anonymous), AHole _ -> sigma
-  | PatCstr (loc,(ind,_ as r1),[],_), ARef (ConstructRef r2) when r1 = r2 ->
-      sigma
+let rec match_cases_pattern metas sigma a1 a2 =
+  let match_cases_pattern_no_more_args metas sigma a1 a2 =
+    match match_cases_pattern metas sigma a1 a2 with
+      |out,[] -> out
+      |_ -> raise No_match in
+ match (a1,a2) with
+  | r1, AVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[]
+  | PatVar (_,Anonymous), AHole _ -> sigma,[]
+  | PatCstr (loc,(ind,_ as r1),largs,_), ARef (ConstructRef r2) when r1 = r2 ->
+      sigma,largs
   | PatCstr (loc,(ind,_ as r1),args1,_), AApp (ARef (ConstructRef r2),l2)
       when r1 = r2 ->
-      let nparams = Inductive.inductive_params (Global.lookup_inductive ind) in
-      if List.length l2 <> nparams + List.length args1
+      let l1 = add_patterns_for_params r1 args1 in
+      let le2 = List.length l2 in
+      if le2 > List.length l1
       then
-	(* TODO: revert partially applied notations of the form
-           "Notation P := (@pair)." *)
 	raise No_match
       else
-        let (p2,args2) = list_chop nparams l2 in
-        (* All parameters must be _ *)
-        List.iter (function AHole _ -> () | _ -> raise No_match) p2;
-	List.fold_left2 (match_cases_pattern metas) sigma args1 args2
+	let l1',more_args = Util.list_chop le2 l1 in
+	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args
   | r1, AList (x,_,iter,termin,lassoc) ->
-      match_alist (fun (metas,_) -> match_cases_pattern metas)
-	(metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc
+      (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas)
+	(metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),[]
   | _ -> raise No_match
 
 let match_aconstr_cases_pattern c (metas,pat) =
   let vars = List.map fst metas in
-  let terms,termlists,() = match_cases_pattern vars ([],[],()) c pat in
+  let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in
   (* Reorder canonically the substitution *)
-  List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
+  (List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
     match typ with
     | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists')
     | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists')
     | NtnTypeBinderList -> assert false)
-    metas ([],[])
+    metas ([],[])),more_args
 
 (**********************************************************************)
 (*s Concrete syntax for terms *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 4527dc48a4..66aa1ba58c 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -98,7 +98,7 @@ val match_aconstr : bool -> glob_constr -> interpretation ->
       (glob_decl list * subscopes) list
 
 val match_aconstr_cases_pattern :  cases_pattern -> interpretation ->
-      (cases_pattern * subscopes) list * (cases_pattern list * subscopes) list
+      ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list)
 
 (** Substitution of kernel names in interpretation data                *)