Fix bug in subst_cases_pattern when aliasing recursive notations.

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

2 files changed, 19 insertions, 21 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f5ad4172c..2e5ec38c8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -424,17 +424,17 @@ 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
 
-let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a =
-  let rec aux aliases subst = function
+let subst_cases_pattern loc alias intern subst scopes a =
+  let rec aux alias subst = function
   | AVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
 	(* of the notations *)
 	try 
 	  let (a,(scopt,subscopes)) = List.assoc id subst in
-	  intern (subscopes@scopes) ([],[]) scopt a
+	    intern (subscopes@scopes) ([],[]) scopt a
 	with Not_found -> 
-	  if id = ldots_var then [],[[], PatVar (loc,Name id)] else
+	  if id = ldots_var then [], [[], PatVar (loc,Name id)] else
 	  anomaly ("Unbound pattern notation variable: "^(string_of_id id))
 	  (*
 	  (* Happens for local notation joint with inductive/fixpoint defs *)
@@ -444,33 +444,34 @@ let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a =
 	  *)
       end
   | ARef (ConstructRef c) ->
-      (ids,[asubst, PatCstr (loc,c, [], alias_of aliases)])
+      ([],[[], PatCstr (loc,c, [], alias)])
   | AApp (ARef (ConstructRef (ind,_ as c)),args) ->
       let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
       let _,args = list_chop nparams args in
-      let idslpll = List.map (aux ([],[]) subst) args in
-      let ids',pll = product_of_cases_patterns ids idslpll in
+      let idslpll = List.map (aux Anonymous subst) args in
+      let ids',pll = product_of_cases_patterns [] idslpll in
       let pl' = List.map (fun (subst,pl) -> 
-        subst,PatCstr (loc,c,pl,alias_of aliases)) pll in
-      ids', pl'
+        subst,PatCstr (loc,c,pl,alias)) pll in
+	ids', pl'
   | AList (x,_,iter,terminator,lassoc) ->
       (try 
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (a,(scopt,subscopes)) = List.assoc x subst in
-        let termin = aux ([],[]) subst terminator in
+        let termin = aux Anonymous subst terminator in
         let l = decode_patlist_value a in
         let idsl,v =
 	  List.fold_right (fun a (tids,t) -> 
-            let uids,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in
+            let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst) iter in
             let pll = List.map (subst_pat_iterator ldots_var t) u in
             tids@uids, List.flatten pll)
             (if lassoc then List.rev l else l) termin in
-        ids@idsl, v
+        idsl, List.map (fun ((subst, pl) as x) -> 
+	  match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v
       with Not_found -> 
           anomaly "Inconsistent substitution of recursive notation")
   | t -> user_err_loc (loc,"",str "Invalid notation for pattern")
-  in aux aliases subst a
-
+  in aux alias subst a
+    
 (* Differentiating between constructors and matching variables *)
 type pattern_qualid_kind =
   | ConstrPat of (constructor * cases_pattern list)
@@ -565,11 +566,12 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
       intern_cases_pattern genv scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
-      let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+      let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
       if !dump then dump_notation_location (patntn_loc loc args ntn) df;
-      let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-      subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes 
+      let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
+      let ids'',pl = subst_cases_pattern loc (alias_of aliases) (intern_cases_pattern genv) subst scopes 
 	c
+      in ids@ids'', pl
   | CPatPrim (loc, p) ->
       let a = alias_of aliases in
       let (c,df) = Notation.interp_prim_token_cases_pattern loc p a 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index edbf9fb62..eac01a92a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -61,10 +61,6 @@ val intern_pattern : env -> cases_pattern_expr ->
   Names.identifier list *
     ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
 
-val intern_pattern : env -> cases_pattern_expr ->
-  Names.identifier list *
-    ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
-
 (*s Composing internalisation with pretyping *)
 
 (* Main interpretation function *)