Prise en compte des scopes traversés dans les notations

Traitement spécial pour le scope type_scope à l'internalisation
Ajout "Locate Notation"


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

10 files changed, 197 insertions, 153 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9e792dc744..cda51446e3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -111,13 +111,27 @@ let add_glob loc ref =
   dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id)
 
 (**********************************************************************)
+(* Remembering the parsing scope of variables in notations            *)
+
+let set_var_scope loc id (_,_,scopes) (_,_,varscopes) =
+  try 
+    let idscopes = List.assoc id varscopes in
+    if !idscopes <> None & !idscopes <> Some scopes then
+      user_err_loc (loc,"set_var_scope",
+        pr_id id ++ str " already occurs in a different scope")
+    else
+      idscopes := Some scopes
+  with Not_found ->
+    if_verbose warning ("Could not globalize " ^ (string_of_id id))
+
+(**********************************************************************)
 (* Discriminating between bound variables and global references       *)
 
 (* [vars1] is a set of name to avoid (used for the tactic language);
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-let intern_var (env,impls,_) (vars1,vars2) loc id =
+let intern_var (env,impls,scopes) (vars1,vars2,_) loc id =
   (* Is [id] bound in  *)
   if Idset.mem id env or List.mem id vars1
   then
@@ -157,13 +171,13 @@ let intern_reference env lvar = function
       with e ->
 	(* Extra allowance for grammars *)
 	if !interning_grammar then begin
-	  if_verbose warning ("Could not globalize " ^ (string_of_id id));
-	  RVar (loc, id), [], []
+	  set_var_scope loc id env lvar;
+	  RVar (loc,id), [], []
 	end
 	else raise e
 
 let interp_reference vars r =
-  let (r,_,_) = intern_reference (Idset.empty,[],[]) (vars,[]) r in r
+  let (r,_,_) = intern_reference (Idset.empty,[],[]) (vars,[],[]) r in r
 
 let apply_scope_env (ids,impls,scopes as env) = function
   | [] -> env, []
@@ -351,8 +365,8 @@ let rec subst_rawconstr loc interp subst (ids,impls,scopes as env) = function
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let internalise sigma env allow_soapp lvar c =
-  let rec intern (ids,impls,scopes as env) = function
+let internalise isarity sigma env allow_soapp lvar c =
+  let rec intern isarity (ids,impls,scopes as env) = function
     | CRef ref as x ->
 	let (c,imp,subscopes) = intern_reference env lvar ref in
 	(match intern_impargs c env imp subscopes [] with
@@ -367,8 +381,9 @@ let internalise sigma env allow_soapp lvar c =
 	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
 	in
 	let ids' = List.fold_right Idset.add lf ids in
-	let defl = Array.of_list (List.map (intern (ids',impls,scopes)) lt) in
-	let arityl = Array.of_list (List.map (intern env) lc) in
+	let defl =
+	  Array.of_list (List.map (intern false (ids',impls,scopes)) lt) in
+	let arityl = Array.of_list (List.map (intern true env) lc) in
 	RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
     | CCoFix (loc, (locid,iddef), ldecl) ->
 	let (lf,lc,lt) = intern_cofix ldecl in
@@ -379,30 +394,32 @@ let internalise sigma env allow_soapp lvar c =
 	    raise (InternalisationError (locid,UnboundFixName (true,iddef)))
 	in
 	let ids' = List.fold_right Idset.add lf ids in
-	let defl = Array.of_list (List.map (intern (ids',impls,scopes)) lt) in
-	let arityl = Array.of_list (List.map (intern env) lc) in
+	let defl =
+	  Array.of_list (List.map (intern false (ids',impls,scopes)) lt) in
+	let arityl = Array.of_list (List.map (intern true env) lc) in
 	RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
     | CArrow (loc,c1,c2) ->
-        RProd (loc, Anonymous, intern env c1, intern env c2)
+        RProd (loc, Anonymous, intern true env c1, intern true env c2)
     | CProdN (loc,[],c2) ->
-        intern env c2
+        intern true env c2
     | CProdN (loc,(nal,ty)::bll,c2) ->
         iterate_prod loc env ty (CProdN (loc, bll, c2)) nal
     | CLambdaN (loc,[],c2) ->
-        intern env c2
+        intern isarity env c2
     | CLambdaN (loc,(nal,ty)::bll,c2) ->
-	iterate_lam loc env ty (CLambdaN (loc, bll, c2)) nal
+	iterate_lam loc isarity env ty (CLambdaN (loc, bll, c2)) nal
     | CLetIn (loc,(_,na),c1,c2) ->
-	RLetIn (loc, na, intern env c1,
-          intern (name_fold Idset.add na ids,impls,scopes) c2)
+	RLetIn (loc, na, intern false env c1,
+          intern false (name_fold Idset.add na ids,impls,scopes) c2)
     | CNotation (loc,ntn,args) ->
+	let scopes = if isarity then Symbols.type_scope::scopes else scopes in
 	let (ids,c) = Symbols.interp_notation ntn scopes in
 	let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-	subst_rawconstr loc intern subst env c
+	subst_rawconstr loc (intern false) subst env c
     | CNumeral (loc, n) ->
 	Symbols.interp_numeral loc n scopes
     | CDelimiters (loc, key, e) ->
-	intern (ids,impls,find_delimiters_scope loc key::scopes) e
+	intern isarity (ids,impls,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, ref, args) ->
         let (f,_,args_scopes) = intern_reference env lvar ref in
 	RApp (loc, f, intern_args env args_scopes args)
@@ -410,16 +427,17 @@ let internalise sigma env allow_soapp lvar c =
 	let (c, impargs, args_scopes) =
 	  match f with
 	    | CRef ref -> intern_reference env lvar ref
-	    | _ -> (intern env f, [], [])
+	    | _ -> (intern false env f, [], [])
         in
 	  RApp (loc, c, intern_impargs c env impargs args_scopes args)
     | CCases (loc, po, tms, eqns) ->
-	RCases (loc, option_app (intern env) po,
-		List.map (intern env) tms,
+	RCases (loc, option_app (intern true env) po,
+		List.map (intern false env) tms,
 		List.map (intern_eqn (List.length tms) env) eqns)
     | COrderedCase (loc, tag, po, c, cl) ->
-	ROrderedCase (loc, tag, option_app (intern env) po, intern env c,
-		  Array.of_list (List.map (intern env) cl))
+	ROrderedCase (loc, tag, option_app (intern true env) po,
+	          intern false env c,
+		  Array.of_list (List.map (intern false env) cl))
     | CHole loc -> 
 	RHole (loc, QuestionMark)
     | CMeta (loc, n) when n >=0 or allow_soapp ->
@@ -429,7 +447,7 @@ let internalise sigma env allow_soapp lvar c =
     | CSort (loc, s) ->
 	RSort(loc,s)
     | CCast (loc, c1, c2) ->
-	RCast (loc,intern env c1,intern env c2)
+	RCast (loc,intern false env c1,intern true env c2)
 
     | CDynamic (loc,d) -> RDynamic (loc,d)
 
@@ -446,24 +464,24 @@ let internalise sigma env allow_soapp lvar c =
 	let rhs = replace_vars_constr_expr subst rhs in
 	List.iter message_redundant_alias subst;
 	let env_ids = List.fold_right Idset.add eqn_ids ids in
-	(loc, eqn_ids,pl,intern (env_ids,impls,scopes) rhs)
+	(loc, eqn_ids,pl,intern false (env_ids,impls,scopes) rhs)
 
   and iterate_prod loc2 (ids,impls,scopes as env) ty body = function
     | (loc1,na)::nal ->
 	if nal <> [] then check_capture loc1 ty na;
 	let ids' = name_fold Idset.add na ids in
 	let body = iterate_prod loc2 (ids',impls,scopes) ty body nal in
-	RProd (join_loc loc1 loc2, na, intern env ty, body)
-    | [] -> intern env body
+	RProd (join_loc loc1 loc2, na, intern true env ty, body)
+    | [] -> intern true env body
 
-  and iterate_lam loc2 (ids,impls,scopes as env) ty body = function
+  and iterate_lam loc2 isarity (ids,impls,scopes as env) ty body = function
     | (loc1,na)::nal ->
 	if nal <> [] then check_capture loc1 ty na;
 	let ids' = name_fold Idset.add na ids in
-	let body = iterate_lam loc2 (ids',impls,scopes) ty body nal in
-	let ty = locate_if_isevar loc1 na (intern env ty) in
+	let body = iterate_lam loc2 isarity (ids',impls,scopes) ty body nal in
+	let ty = locate_if_isevar loc1 na (intern true env ty) in
 	RLambda (join_loc loc1 loc2, na, ty, body)
-    | [] -> intern env body
+    | [] -> intern isarity env body
 
   and intern_impargs c env l subscopes args =
     let rec aux n l subscopes args = 
@@ -472,7 +490,7 @@ let internalise sigma env allow_soapp lvar c =
       | (imp::l', (a,Some j)::args') ->
 	  if is_status_implicit imp & j>=n then
 	    if j=n then 
-	      (intern enva a)::(aux (n+1) l' subscopes' args')
+	      (intern false enva a)::(aux (n+1) l' subscopes' args')
 	    else 
 	      (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
 	  else 
@@ -483,7 +501,7 @@ let internalise sigma env allow_soapp lvar c =
 	  if is_status_implicit imp then 
 	    (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
 	  else 
-	    (intern enva a)::(aux (n+1) l' subscopes' args')
+	    (intern false enva a)::(aux (n+1) l' subscopes' args')
       | ([],args) -> intern_tailargs env subscopes args
       | (_::l',[]) ->
           if List.for_all is_status_implicit l then
@@ -497,18 +515,18 @@ let internalise sigma env allow_soapp lvar c =
 	raise (InternalisationError (constr_loc a, WrongExplicitImplicit))
     | (a,None)::args ->
       let (enva,subscopes) = apply_scope_env env subscopes in
-      (intern enva a) :: (intern_tailargs env subscopes args)
+      (intern false enva a) :: (intern_tailargs env subscopes args)
     | [] -> []
 
   and intern_args env subscopes = function
     | [] -> []
     | a::args ->
         let (enva,subscopes) = apply_scope_env env subscopes in
-        (intern enva a) :: (intern_args env subscopes args)
+        (intern false enva a) :: (intern_args env subscopes args)
 
   in 
   try 
-    intern env c
+    intern isarity env c
   with
       InternalisationError (loc,e) ->
 	user_err_loc (loc,"internalize",explain_internalisation_error e)
@@ -522,21 +540,26 @@ let extract_ids env =
     (Termops.ids_of_rel_context (Environ.rel_context env))
     Idset.empty
 
-let interp_rawconstr_gen sigma env impls allow_soapp lvar c =
-  internalise sigma (extract_ids env, impls, Symbols.current_scopes ())
-    allow_soapp (lvar,Environ.named_context env) c
+let interp_rawconstr_gen isarity sigma env impls allow_soapp lvar c =
+  internalise isarity sigma (extract_ids env, impls, [])
+    allow_soapp (lvar,Environ.named_context env, []) c
 
 let interp_rawconstr sigma env c =
-  interp_rawconstr_gen sigma env [] false [] c
+  interp_rawconstr_gen false sigma env [] false [] c
+
+let interp_rawtype sigma env c =
+  interp_rawconstr_gen true sigma env [] false [] c
 
-let interp_rawconstr_with_implicits sigma env impls c =
-  interp_rawconstr_gen sigma env impls false [] c
+let interp_rawtype_with_implicits sigma env impls c =
+  interp_rawconstr_gen true sigma env impls false [] c
 
+(*
 (* The same as interp_rawconstr but with a list of variables which must not be
    globalized *)
 
 let interp_rawconstr_wo_glob sigma env lvar c =
   interp_rawconstr_gen sigma env [] false lvar c
+*)
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
@@ -551,10 +574,10 @@ let interp_casted_openconstr sigma env c typ =
   understand_gen_tcc sigma env [] [] (Some typ) (interp_rawconstr sigma env c)
 
 let interp_type sigma env c =
-  understand_type sigma env (interp_rawconstr sigma env c)
+  understand_type sigma env (interp_rawtype sigma env c)
 
 let interp_type_with_implicits sigma env impls c =
-  understand_type sigma env (interp_rawconstr_with_implicits sigma env impls c)
+  understand_type sigma env (interp_rawtype_with_implicits sigma env impls c)
 
 let judgment_of_rawconstr sigma env c =
   understand_judgment sigma env (interp_rawconstr sigma env c)
@@ -574,14 +597,14 @@ let retype_list sigma env lst =
 (* of instantiations (variables and metas)    *)
 (* Note: typ is retyped *)
 let interp_constr_gen sigma env lvar lmeta c exptyp =
-  let c = interp_rawconstr_gen sigma env [] false (List.map fst lvar) c
+  let c = interp_rawconstr_gen false sigma env [] false (List.map fst lvar) c
   and rtype lst = retype_list sigma env lst in
   understand_gen sigma env (rtype lvar) (rtype lmeta) exptyp c;;
 
 (*Interprets a casted constr according to two lists of instantiations
   (variables and metas)*)
 let interp_openconstr_gen sigma env lvar lmeta c exptyp =
-  let c = interp_rawconstr_gen sigma env [] false (List.map fst lvar) c
+  let c = interp_rawconstr_gen false sigma env [] false (List.map fst lvar) c
   and rtype lst = retype_list sigma env lst in
   understand_gen_tcc sigma env (rtype lvar) (rtype lmeta) exptyp c;;
 
@@ -636,12 +659,21 @@ let pattern_of_rawconstr lvar c =
   (!metas,p)
 
 let interp_constrpattern_gen sigma env lvar c =
-  let c = interp_rawconstr_gen sigma env [] true (List.map fst lvar) c in
+  let c = interp_rawconstr_gen false sigma env [] true (List.map fst lvar) c in
   let nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in
   pattern_of_rawconstr nlvar c
 
 let interp_constrpattern sigma env c =
   interp_constrpattern_gen sigma env [] c
 
-let interp_aconstr a =
-  aconstr_of_rawconstr (interp_rawconstr Evd.empty (Global.env()) a)
+let interp_aconstr vars a =
+  let env = Global.env () in
+  (* [vl] is intended to remember the scope of the free variables of [a] *)
+  let vl = List.map (fun id -> (id,ref None)) vars in
+  let c = for_grammar (internalise false Evd.empty (extract_ids env, [], [])
+    false ([],Environ.named_context env,vl)) a in
+  (* Translate and check that [c] has all its free variables bound in [vars] *)
+  let a = aconstr_of_rawconstr vars c in
+  (* Returns [a] and the ordered list of variables with their scopes *)
+  (* Variables occuring in binders have no relevant scope since bound *)
+  List.map (fun (id,r) -> (id,match !r with None -> [] | Some l -> l)) vl, a
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 8666db6338..4c185a788e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -36,7 +36,7 @@ type implicits_env = (identifier * Impargs.implicits_list) list
 
 (* Interprets global names, including syntactic defs and section variables *)
 val interp_rawconstr     : evar_map -> env -> constr_expr -> rawconstr
-val interp_rawconstr_gen : evar_map -> env -> implicits_env -> 
+val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> 
     bool -> identifier list -> constr_expr -> rawconstr
 
 (*s Composing the translation with typing *)
@@ -83,7 +83,7 @@ val interp_constrpattern :
 val interp_reference : identifier list -> reference -> rawconstr
 
 (* Interprets into a abbreviatable constr *)
-val interp_aconstr : constr_expr -> aconstr
+val interp_aconstr : identifier list -> constr_expr -> interpretation
 
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/symbols.ml b/interp/symbols.ml
index 6fc3c93c09..6a02f284b1 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -58,8 +58,9 @@ let empty_scope = {
 let default_scope = "core_scope"
 let type_scope = "type_scope"
 
-let _ = Stringmap.add default_scope empty_scope !scope_map
-let _ = Stringmap.add type_scope empty_scope !scope_map
+let init_scope_map () =
+  scope_map := Stringmap.add default_scope empty_scope !scope_map;
+  scope_map := Stringmap.add type_scope empty_scope !scope_map
 
 (**********************************************************************)
 (* The global stack of scopes                                         *)
@@ -225,7 +226,7 @@ let rec find_interpretation f = function
 
 let rec interp_notation ntn scopes =
   let f scope = fst (Stringmap.find ntn scope.notations) in
-  try find_interpretation f scopes
+  try find_interpretation f (scopes @ !scope_stack)
   with Not_found -> anomaly ("Unknown interpretation for notation "^ntn)
 
 let uninterp_notations c =
@@ -236,24 +237,22 @@ let availability_of_notation (ntn_scope,ntn) scopes =
     Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
   find_without_delimiters f ntn_scope scopes
 
-let rec interp_numeral loc n = function
+let rec interp_numeral_gen loc f n = function
   | scope :: scopes ->
-      (try fst (lookup_numeral_interpreter loc scope) loc n
-       with Not_found -> interp_numeral loc n scopes)
+      (try f (lookup_numeral_interpreter loc scope)
+       with Not_found -> interp_numeral_gen loc f n scopes)
   | [] ->
       user_err_loc (loc,"interp_numeral",
       str "No interpretation for numeral " ++ pr_bigint n)
 
-let rec interp_numeral_as_pattern loc n name = function
-  | scope :: scopes ->
-      (try 
-	match snd (lookup_numeral_interpreter loc scope) with
-	  | None -> raise Not_found
-	  | Some g -> g loc n name
-	with Not_found -> interp_numeral_as_pattern loc n name scopes)
-  | [] ->
-      user_err_loc (loc,"interp_numeral_as_pattern",
-      str "No interpretation for numeral " ++ pr_bigint n)
+let interp_numeral loc n scopes =
+  interp_numeral_gen loc (fun x -> fst x loc n) n (scopes@ !scope_stack)
+
+let interp_numeral_as_pattern loc n name scopes =
+  let f x = match snd x with
+    | None -> raise Not_found
+    | Some g -> g loc n name in
+  interp_numeral_gen loc f n (scopes@ !scope_stack)
 
 let uninterp_numeral c =
   try 
@@ -365,6 +364,34 @@ let pr_scopes prraw =
    (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
    !scope_map (mt ())
 
+let rec find_default ntn = function
+  | scope::_ when Stringmap.mem ntn (find_scope scope).notations -> scope
+  | _::scopes -> find_default ntn scopes
+  | [] -> raise Not_found
+
+let locate_notation prraw ntn =
+  let ntn = if String.contains ntn ' ' then ntn else "_ "^ntn^" _" in
+  let l = 
+    Stringmap.fold 
+      (fun scope_name sc l ->
+	try
+	  let ((_,r),(_,df)) = Stringmap.find ntn sc.notations in
+	  (scope_name,r,df)::l
+	with Not_found -> l) !scope_map []
+  in
+  if l = [] then
+    str "Unknown notation"
+  else
+    let scope = find_default ntn !scope_stack in
+    prlist 
+      (fun (sc,r,df) ->
+	hov 0 (
+	  pr_notation_info prraw df r ++ brk (1,2) ++
+	  str ": " ++ str sc ++ 
+	  (if sc = scope then str " (default interpretation)" else mt ()) ++
+	  fnl ()))
+      l
+
 (**********************************************************************)
 (* Mapping notations to concrete syntax *)
 
@@ -397,8 +424,8 @@ let unfreeze (scm,scs,asc,dlm,fkm,pprules) =
   printing_rules := pprules
 
 let init () =
+  init_scope_map ();
 (*
-  scope_map := Stringmap.empty;
   scope_stack := Stringmap.empty
   arguments_scope := Refmap.empty
 *)
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 17b99dbd42..c8c844312d 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -33,6 +33,7 @@ type scope
 type scopes = scope_name list
 
 val default_scope : scope_name
+val type_scope : scope_name
 val declare_scope : scope_name -> unit
 
 (* Open scope *)
@@ -114,6 +115,7 @@ val find_arguments_scope : global_reference -> scope_name option list
 (* Prints scopes (expect a pure aconstr printer *)
 val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
 val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
+val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds
 
 (**********************************************************************)
 (*s Printing rules for notations *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7c1e9aea5e..aa78ec5e04 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -136,15 +136,26 @@ let rec subst_aconstr subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  ACast (r1',r2')
 
-let rec aux = function
-  | RVar (_,id) -> AVar id
+let add_name r = function
+  | Anonymous -> ()
+  | Name id -> r := id :: !r
+
+let aconstr_of_rawconstr vars a =
+  let found = ref [] in
+  let bound_binders = ref [] in
+  let rec aux = function
+  | RVar (_,id) -> 
+      if not (List.mem id !bound_binders) then found := id::!found;
+      AVar id
   | RApp (_,g,args) -> AApp (aux g, List.map aux args)
-  | RLambda (_,na,ty,c) -> ALambda (na,aux ty,aux c)
-  | RProd (_,na,ty,c) -> AProd (na,aux ty,aux c)
-  | RLetIn (_,na,b,c) -> ALetIn (na,aux b,aux c)
+  | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
+  | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
+  | RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c)
   | RCases (_,tyopt,tml,eqnl) ->
-      let eqnl = List.map (fun (_,idl,pat,rhs) -> (idl,pat,aux rhs)) eqnl in
-      ACases (option_app aux tyopt,List.map aux tml, eqnl)
+      let f (_,idl,pat,rhs) =
+        bound_binders := idl@(!bound_binders);
+        (idl,pat,aux rhs) in
+      ACases (option_app aux tyopt,List.map aux tml, List.map f eqnl)
   | ROrderedCase (_,b,tyopt,tm,bv) ->
       AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
   | RCast (_,c,t) -> ACast (aux c,aux t)
@@ -153,10 +164,15 @@ let rec aux = function
   | RRef (_,r) -> ARef r
   | RMeta (_,n) -> AMeta n
   | RDynamic _ | RRec _ | REvar _ ->
-      error "Fixpoints, cofixpoints and existential variables are not \
+      error "Fixpoints, cofixpoints, existential variables and pattern-matching  not \
 allowed in abbreviatable expressions"
-
-let aconstr_of_rawconstr = aux
+  in
+  let a = aux a in
+  let check_type x =
+    if not (List.mem x !found or List.mem x !bound_binders) then
+      error ((string_of_id x)^" is unbound in the right-hand-side") in
+  List.iter check_type vars;
+  a
 
 (* Pattern-matching rawconstr and aconstr *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 35f62478ef..5c452b870b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -43,7 +43,7 @@ val map_aconstr_with_binders_loc : loc ->
 
 val subst_aconstr : Names.substitution -> aconstr -> aconstr
 
-val aconstr_of_rawconstr : rawconstr -> aconstr
+val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
 
 (* [match_aconstr metas] match a rawconstr against an aconstr with
    metavariables in [metas]; it raises [No_match] if the matching fails *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 283de9ade0..81ee49bd65 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -118,11 +118,13 @@ let declare_definition ident local bl red_option c typopt =
     | (Global|Local) ->
         declare_global_definition ident ce' local
 
+
 let syntax_definition ident c =
-  let c = interp_aconstr c in 
+  let c = snd (interp_aconstr [] c) in 
   Syntax_def.declare_syntactic_definition ident c;
   if_verbose message ((string_of_id ident) ^ " is now a syntax macro")
 
+
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
 let assumption_message id =
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index f408c07f48..76005c00e5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -69,60 +69,6 @@ let _ = set_constr_globalizer
 
 let _ = define_ast_quotation true "constr" constr_parser_with_glob
 
-let add_name r = function
-  | Anonymous -> ()
-  | Name id -> r := id :: !r
-
-let make_aconstr vars a =
-  let bound_vars = ref [] in
-  let bound_binders = ref [] in
-  let rec aux = function
-  | RVar (_,id) ->
-      if List.mem id vars then bound_vars := id::!bound_vars;
-      AVar id
-  | RApp (_,g,args) -> AApp (aux g, List.map aux args)
-  | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
-  | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
-  | RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c)
-  | RCases (_,tyopt,tml,eqnl) ->
-      let f (_,idl,pat,rhs) =
-        bound_binders := idl@(!bound_binders);
-        (idl,pat,aux rhs) in
-      ACases (option_app aux tyopt,List.map aux tml, List.map f eqnl)
-  | ROrderedCase (_,b,tyopt,tm,bv) ->
-      AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
-  | RCast (_,c,t) -> ACast (aux c,aux t)
-  | RSort (_,s) -> ASort s
-  | RHole (_,w) -> AHole w
-  | RRef (_,r) -> ARef r
-  | RMeta (_,n) -> AMeta n
-  | RDynamic _ | RRec _ | REvar _ ->
-      error "Fixpoints, cofixpoints, existential variables and pattern-matching  not \
-allowed in abbreviatable expressions"
-  in
-  let a = aux a in
-  let find_type x =
-    if List.mem x !bound_binders then (x,ETIdent) else
-    if List.mem x !bound_vars then (x,ETConstr (10,())) else
-      error ((string_of_id x)^" is unbound in the right-hand-side") in
-  let typs = List.map find_type vars in
-  (a, typs)
-
-(*
-let _ = set_grammar_globalizer
-  (fun vl a ->
-    let r = for_grammar (globalize_constr_expr [] vl) a in
-    let a, typs = make_aconstr vl r in
-(*
-    List.iter2
-      (fun (x,typ) (x',typ') ->
-	assert (x=x');
-	if typ = ETConstr & typ' = ETIdent then
-	  error "cannot use a constr parser to parse an ident") etyps typs;
-*)
-    a)
-*)
-
 (** For old ast printer *)
 
 (* Pretty-printer state summary *)
@@ -269,7 +215,7 @@ let meta_pattern m = Pmeta(m,Tany)
 
 open Symbols
 
-type white_status = Juxtapose | Separate of int
+type white_status = Juxtapose | Separate of int | NextIsTerminal
 
 let add_break l = function
   | Separate n -> UNP_BRK (n,1) :: l
@@ -317,8 +263,20 @@ let make_hunks_ast symbols etyps from =
 
 let add_break l = function
   | Separate n -> UnpCut (PpBrk(n,1)) :: l
+  | NextIsTerminal -> UnpCut (PpBrk(1,1)) :: l
   | _ -> l
 
+let is_bracket s =
+  let l = String.length s in l <> 0 &
+  (s.[0] = '{' or s.[0] = '[' or s.[0] = '(' or
+   s.[l-1] = '}' or s.[l-1] = ']' or s.[l-1] = ')')
+
+let is_operator s =
+  let l = String.length s in l <> 0 &
+  (s.[0] = '+' or s.[0] = '*' or s.[0] = '=' or
+   s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or
+   s.[0] = '@')
+
 let make_hunks etyps symbols =
   let vars,typs = List.split etyps in
   let (_,l) =
@@ -329,20 +287,26 @@ let make_hunks etyps symbols =
 	  let _,prec = precedence_of_entry_type (List.nth typs (i-1)) in
 	  let u = UnpMetaVar (i ,prec) in
 	  let l' = u :: (add_break l ws) in
-	  (Separate 1, l')
+	  (NextIsTerminal, l')
       | Terminal s ->
-	    let n,(s,l) =
+	    let nextsep,(s,l) =
 	      if
 		is_letter (s.[0]) or 
 		is_letter (s.[String.length s -1]) or
 		is_digit (s.[String.length s -1])
 	      then
 		(* We want spaces around both sides *)
-		1, if ws = Separate 0 then s^" ",l else s,add_break l ws
+		Separate 1,
+		if ws = Separate 0 then s^" ",l else s,add_break l ws
 	      else
-		(* We want a break before symbols, hence [Separate 0] *)
-		0, (s,l) in
-	    (Separate n, UnpTerminal s :: l)
+		(* We want a break before symbols but brackets*)
+		if is_bracket s then
+		  Juxtapose,
+		  (s,if ws = Separate 0 then add_break l ws else l)
+		 else
+		  Separate 0, (s,l)
+	    in
+	    (nextsep, UnpTerminal s :: l)
       | Break n ->
 	    (Juxtapose, UnpCut (PpBrk (n,1)) :: l))
     symbols (Juxtapose,[])
@@ -447,7 +411,7 @@ let make_syntax_rule n name symbols typs ast ntn sc =
       [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}]
 
 let make_pp_rule symbols typs =
-  [UnpBox (PpHOVB 1, make_hunks symbols typs)]
+  [UnpBox (PpHOVB 0, make_hunks symbols typs)]
 
 
 (**************************************************************************)
@@ -623,7 +587,7 @@ let make_old_pp_rule n symbols typs r ntn scope vars =
   let rule_name = ntn^"_"^scope^"_notation" in
   make_syntax_rule n rule_name symbols typs ast ntn scope
 
-let add_notation_in_scope df a (assoc,n,etyps,onlyparse) sc toks =
+let add_notation_in_scope df c (assoc,n,etyps,onlyparse) sc toks =
   let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
   let (typs,symbols) =
     find_symbols
@@ -631,12 +595,7 @@ let add_notation_in_scope df a (assoc,n,etyps,onlyparse) sc toks =
       [] toks in
   let vars = List.map fst typs in
   (* To globalize... *)
-  let r = interp_rawconstr_gen Evd.empty (Global.env()) [] false vars a in
-  let a,_ = make_aconstr vars r in
-(*
-  let a,etyps' = make_aconstr vars r in
-  let etyps = merge_entry_types etyps' etyps in
-*)
+  let a = interp_aconstr vars c in
   let typs = List.map (set_entry_type etyps) typs in
   let assoc = recompute_assoc typs in
   (* Declare the parsing and printing rules if not already done *)
@@ -646,11 +605,14 @@ let add_notation_in_scope df a (assoc,n,etyps,onlyparse) sc toks =
   Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule));
   let old_pp_rule =
     if onlyparse then None
-    else Some (make_old_pp_rule n symbols typs r notation scope vars) in
+    else 
+      let r = 
+	interp_rawconstr_gen false Evd.empty (Global.env()) [] false vars c in
+      Some (make_old_pp_rule n symbols typs r notation scope vars) in
   (* Declare the interpretation *)
   let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
   Lib.add_anonymous_leaf
-    (inNotation(old_pp_rule,prec,notation,scope,(vars,a),onlyparse,df))
+    (inNotation(old_pp_rule,prec,notation,scope,a,onlyparse,df))
 
 let add_notation df a modifiers sc =
   let toks = split df in
@@ -658,7 +620,8 @@ let add_notation df a modifiers sc =
     | [String x] when quote(strip x) = x & modifiers = [] ->
         (* Means a Syntactic Definition *)
         let ident = id_of_string (strip x) in
-        Syntax_def.declare_syntactic_definition ident (interp_aconstr a)
+	let c = snd (interp_aconstr [] a) in
+        Syntax_def.declare_syntactic_definition ident c
     | _ ->
        add_notation_in_scope df a (interp_notation_modifiers modifiers) sc toks
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 99b2444c0e..13acd292c1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -847,7 +847,8 @@ let vernac_locate = function
   | LocateTerm qid -> print_located_qualid qid
   | LocateLibrary qid -> print_located_library qid
   | LocateFile f -> locate_file f
-
+  | LocateNotation ntn ->
+      ppnl (Symbols.locate_notation (Constrextern.without_symbols pr_rawterm) ntn)
 
 (********************)
 (* Proof management *)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index a7ee9a57b9..c0726c0253 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -67,6 +67,7 @@ type locatable =
   | LocateTerm of reference
   | LocateLibrary of reference
   | LocateFile of string
+  | LocateNotation of notation
 
 type goable =
   | GoTo of int