Fixup implicits in patterns & notations

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

3 files changed, 14 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5fec962b8..3c3858f29 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -423,7 +423,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 		      |Some true_args -> CPatCstr (loc, c, [], true_args)
 		      |None -> CPatCstr (loc, c, full_args, [])
 	  in insert_pat_alias loc p na
-and apply_notation_to_pattern loc gr ((subst,substlist),more_args)
+and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
     (tmp_scope, scopes as allscopes) vars =
   function
     | NotationRule (sc,ntn) ->
@@ -446,7 +446,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),more_args)
 	    let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
 	    let l2' = if !Topconstr.oldfashion_patterns || ll <> [] then l2
 	      else
-		match drop_implicits_in_patt gr (List.length l) l2 with
+		match drop_implicits_in_patt gr nb_to_drop l2 with
 		  |Some true_args -> true_args
 		  |None -> raise No_match
 	    in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 857e827a9..fb025be6f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -748,10 +748,10 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
 
 let rec match_cases_pattern metas sigma a1 a2 =
  match (a1,a2) with
-  | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[]
-  | PatVar (_,Anonymous), NHole _ -> sigma,[]
+  | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
+  | PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
   | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when r1 = r2 ->
-      sigma,largs
+      sigma,(0,largs)
   | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
       when r1 = r2 ->
       let l1 = add_patterns_for_params (fst r1) args1 in
@@ -761,21 +761,21 @@ let rec match_cases_pattern metas sigma a1 a2 =
 	raise No_match
       else
 	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
+	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
   | r1, NList (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),[]
+	(metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),(0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
     match match_cases_pattern metas sigma a1 a2 with
-      |out,[] -> out
+      |out,(_,[]) -> out
       |_ -> raise No_match
 
 let match_ind_pattern metas sigma ind pats a2 =
   match a2 with
   | NRef (IndRef r2) when ind = r2 ->
-      sigma,pats
+      sigma,(0,pats)
   | NApp (NRef (IndRef r2),l2)
       when ind = r2 ->
       let le2 = List.length l2 in
@@ -784,7 +784,7 @@ let match_ind_pattern metas sigma ind pats a2 =
 	raise No_match
       else
 	let l1',more_args = Util.list_chop le2 pats in
-	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args
+	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
   |_ -> raise No_match
 
 let reorder_canonically_substitution terms termlists metas =
@@ -798,9 +798,9 @@ let reorder_canonically_substitution terms termlists metas =
 let match_notation_constr_cases_pattern c (metas,pat) =
   let vars = List.map fst metas in
   let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in
-  reorder_canonically_substitution terms termlists metas,more_args
+  reorder_canonically_substitution terms termlists metas, more_args
 
 let match_notation_constr_ind_pattern ind args (metas,pat) =
   let vars = List.map fst metas in
   let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in
-  reorder_canonically_substitution terms termlists metas,more_args
+  reorder_canonically_substitution terms termlists metas, more_args
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index ef92500f1..3389e4a3f 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -47,12 +47,12 @@ val match_notation_constr : bool -> glob_constr -> interpretation ->
 val match_notation_constr_cases_pattern :
   cases_pattern -> interpretation ->
   ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
-    (cases_pattern list)
+    (int * cases_pattern list)
 
 val match_notation_constr_ind_pattern :
   inductive -> cases_pattern  list -> interpretation ->
   ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
-    (cases_pattern list)
+    (int * cases_pattern list)
 
 (** Substitution of kernel names in interpretation data                *)