diff options
| author | herbelin | 2004-04-08 15:21:25 +0000 |
|---|---|---|
| committer | herbelin | 2004-04-08 15:21:25 +0000 |
| commit | b0d199d2f08d42babd9061aff45a9bda0ac68b75 (patch) | |
| tree | 021987625a0f895fe5a2af4612828b69e1b2eae5 /interp/constrintern.ml | |
| parent | 866ef538adffca2bd4e3f8c6846907ebd377216a (diff) | |
Chgt role 2eme argument AList et implantation affichage motifs recursifs de notations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5663 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a3448d74fe..8a16a56db9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -428,7 +428,7 @@ let subst_cases_pattern loc aliases intern subst scopes a = let _,args = list_chop nparams args in let (idsl,pl) = List.split (List.map (aux ([],[]) subst) args) in aliases::List.flatten idsl, PatCstr (loc,c,pl,alias_of aliases) - | AList (x,y,iter,terminator,lassoc) -> + | 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 @@ -437,7 +437,7 @@ let subst_cases_pattern loc aliases intern subst scopes a = let idsl,v = List.fold_right (fun a (allidsl,t) -> let idsl,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in - idsl::allidsl, subst_pat_iterator y t u) + idsl::allidsl, subst_pat_iterator ldots_var t u) (if lassoc then List.rev l else l) ([idslt],termin) in aliases::List.flatten idsl, v with Not_found -> @@ -688,7 +688,7 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) = (* Happens for local notation joint with inductive/fixpoint defs *) RVar (loc,id) end - | AList (x,y,iter,terminator,lassoc) -> + | 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 @@ -697,7 +697,7 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) = terminator in let l = decode_constrlist_value a in List.fold_right (fun a t -> - subst_iterator y t + subst_iterator ldots_var t (subst_aconstr_in_rawconstr loc interp ((x,(a,(scopt,subscopes)))::subst) (ids,None,scopes) iter)) |