Le test de redondance d'une règle était trop fort

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

1 files changed, 8 insertions, 7 deletions

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