Fixed a bug introduced (r13316/r13329) in the printing of notations

with non-recursive binders.

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

1 files changed, 12 insertions, 23 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 231e69ed4..dc35c47db 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -571,7 +571,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | _ -> raise No_match
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
-  | (Name id1,Name id2) when List.mem id2 metas ->
+  | (Name id1,Name id2) when List.mem id2 (fst metas) ->
       alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
@@ -608,7 +608,7 @@ let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
 let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin =
   let rec aux sigma acc rest =
     try
-      let sigma = match_fun (ldots_var::metas) sigma rest iter in
+      let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
       let rest = List.assoc ldots_var (pi1 sigma) in
       let b = match List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false in
       let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
@@ -621,7 +621,7 @@ let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin =
 let match_alist match_fun metas sigma rest x iter termin lassoc =
   let rec aux sigma acc rest =
     try
-      let sigma = match_fun (ldots_var::metas) sigma rest iter in
+      let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
       let rest = List.assoc ldots_var (pi1 sigma) in
       let t = List.assoc x (pi1 sigma) in
       let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
@@ -631,10 +631,10 @@ let match_alist match_fun metas sigma rest x iter termin lassoc =
   let l,sigma = aux sigma [] rest in
   (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma)
 
-let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
+let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with
 
   (* Matching notation variable *)
-  | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
+  | r1, AVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1
 
   (* Matching recursive notations for terms *)
   | r1, AList (x,_,iter,termin,lassoc) ->
@@ -654,11 +654,11 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | r, ABinderList (x,_,iter,termin) ->
       match_abinderlist_with_app (match_ alp) metas sigma r x iter termin
 
-  (* Matching individual binders *)
-  | RLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id metas ->
+  (* Matching individual binders as part of a recursive pattern *)
+  | RLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas ->
       match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
   | RProd (_,na,bk,t,b1), AProd (Name id,_,b2)
-      when List.mem id metas & na <> Anonymous ->
+      when List.mem id blmetas & na <> Anonymous ->
       match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
 
   (* Matching compositionally *)
@@ -739,7 +739,8 @@ and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
   match_ alp metas sigma rhs1 rhs2
 
 let match_aconstr c (metas,pat) =
-  let vars = List.map fst metas in
+  let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
+  let vars = (List.map fst (fst vars), List.map fst (snd vars)) in
   let terms,termlists,binders = match_ [] vars ([],[],[]) c pat in
   (* Reorder canonically the substitution *)
   let find x =
@@ -787,20 +788,8 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
         List.iter (function AHole _ -> () | _ -> raise No_match) p2;
 	List.fold_left2 (match_cases_pattern metas) sigma args1 args2
   | r1, AList (x,_,iter,termin,lassoc) ->
-      match_alist match_cases_pattern
-	metas (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc
-(*
-  | PatCstr (loc,(ind,_ as r1),args1,_),
-    AList (x,y,(AApp (ARef (ConstructRef r2),l2) as iter),termin,lassoc)
-      when r1 = r2 ->
-      let nparams = Inductive.inductive_params (Global.lookup_inductive ind) in
-      assert (List.length args1 + nparams = List.length l2);
-      let (p2,args2) = list_chop nparams l2 in
-      List.iter (function AHole _ -> () | _ -> raise No_match) p2;
-      let x = if lassoc then x else y in
-      match_alist match_cases_pattern
-	metas (pi1 sigma,pi2 sigma,()) args1 args2 x iter termin lassoc
-*)
+      match_alist (fun (metas,_) -> match_cases_pattern metas)
+	(metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc
   | _ -> raise No_match
 
 let match_aconstr_cases_pattern c (metas,pat) =