diff options
| -rw-r--r-- | parsing/symbols.ml | 4 | ||||
| -rw-r--r-- | parsing/symbols.mli | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 15 |
3 files changed, 11 insertions, 10 deletions
diff --git a/parsing/symbols.ml b/parsing/symbols.ml index 075cd322d..21a7575ac 100644 --- a/parsing/symbols.ml +++ b/parsing/symbols.ml @@ -151,8 +151,8 @@ let find_notation pat_scope pat scopes = | Some None -> Some (None,scopes) | Some x -> Some (x,pat_scope::scopes) -let exists_notation_in_scope scope ntn = - try Stringmap.mem ntn (Stringmap.find scope !scope_map).notations +let exists_notation_in_scope scope ntn r = + try Stringmap.find ntn (Stringmap.find scope !scope_map).notations = r with Not_found -> false let exists_notation nt = diff --git a/parsing/symbols.mli b/parsing/symbols.mli index d8edb3179..479977191 100644 --- a/parsing/symbols.mli +++ b/parsing/symbols.mli @@ -44,7 +44,7 @@ val declare_notation : notation -> rawconstr -> scope_name -> unit val interp_notation : notation -> scopes -> rawconstr list -> rawconstr val find_notation : scope_name -> notation -> scopes -> (delimiters option * scopes) option -val exists_notation_in_scope : scope_name -> notation -> bool +val exists_notation_in_scope : scope_name -> notation -> rawconstr -> bool val exists_notation : notation -> bool (* Declare and look for scopes associated to arguments of a global ref *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index cb05a5c7d..e0206e6f7 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -164,7 +164,7 @@ let load_infix _ (_,(gr,se,ntn,scope,pat)) = let open_infix i (_,(gr,se,ntn,scope,pat)) = if i=1 then begin - let b = Symbols.exists_notation_in_scope scope ntn in + let b = Symbols.exists_notation_in_scope scope ntn pat in (* Declare the printer rule and its interpretation *) if not b then Esyntax.add_ppobject {sc_univ="constr";sc_entries=se}; (* Declare the grammar rule ... *) @@ -340,19 +340,20 @@ let make_syntax_rule n name symbols ast ntn sc = let subst_meta_ast subst a = let found = ref [] in + let loc = dummy_loc in let rec subst_rec subst = function - | Smetalam (loc,s,body) -> Smetalam (loc,s,subst_rec subst body) - | Node(loc,"META",_) -> error "Unexpected metavariable in notation" + | Smetalam (_,s,body) -> Smetalam (loc,s,subst_rec subst body) + | Node(_,"META",_) -> error "Unexpected metavariable in notation" | Node(_,"QUALID",[Nvar(_,id)]) as x -> (try let a = List.assoc id subst in found:=id::!found; a with Not_found -> x) - | Node(loc,op,args) -> Node (loc,op, List.map (subst_rec subst) args) - | Slam(loc,None,body) -> Slam(loc,None,subst_rec subst body) - | Slam(loc,Some s,body) -> + | Node(_,op,args) -> Node (loc,op, List.map (subst_rec subst) args) + | Slam(_,None,body) -> Slam(loc,None,subst_rec subst body) + | Slam(_,Some s,body) -> (* Prévenir que "s" peut forcer une capturer à l'instantiation de la *) (* règle de grammaire ?? *) Slam(loc,Some s,subst_rec (List.remove_assoc s subst) body) - | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a + | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> set_loc loc a | Dynamic _ as a -> (* Hum... what to do here *) a in let a = subst_rec subst a in |