diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-03 15:07:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-03 15:07:24 +0000 |
| commit | 02e62e3836e43d993c2bb7168068d3120de08773 (patch) | |
| tree | 5f825ef0e32c93438cba8bdf8776dbc45e4b3be2 /parsing | |
| parent | baed251f7e00024b900c1ddc984cc0fce4df5cb6 (diff) | |
bug de non-indépendance des règles d'affichage et parsing vis à vis du nom des variables de la notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3367 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egrammar.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index c125c4479..7603bde18 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -262,7 +262,7 @@ let subst_constr_expr a loc subs = | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l) | CApp (_,a,l) -> CApp (loc,subst a,List.map (fun (a,i) -> (subst a,i)) l) | CCast (_,a,b) -> CCast (loc,subst a,subst b) - | CNotation (_,n,l) -> CNotation (loc,n,List.map (fun (x,t) ->(x,subst t)) l) + | CNotation (_,n,l) -> CNotation (loc,n,List.map subst l) | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a) | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x | CCases (_,po,a,bl) -> @@ -340,7 +340,7 @@ let extend_constr entry (level,assoc,keepassoc) make_act pt = grammar_extend entry pos [(name, p4assoc, [symbs, act])] let extend_constr_notation (n,assoc,ntn,rule) = - let mkact loc env = CNotation (loc,ntn,env) in + let mkact loc env = CNotation (loc,ntn,List.map snd env) in let (e,level,keepassoc) = get_constr_entry (ETConstr (n,())) in extend_constr e (level,assoc,keepassoc) (make_act mkact) rule |