- Cleanup parsing of binders, reducing to a single production for all

  binders.
- Change syntax of type class instances to better match the usual syntax of
  lemmas/definitions with name first, then arguments ":" instance.
  Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
  documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
  Program.Utils, and subset_scope as well.


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

26 files changed, 205 insertions, 235 deletions

diff --git a/CHANGES b/CHANGES
index 0fd8c3ac6..a349979fc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -129,7 +129,6 @@ Tactic Language
   ltac function into names that do not clash with the lemmas
   parameter names used in the tactic).
 - New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
-  (DOC TODO?)
 - "let rec ... in ... " now supported for expressions without explicit
   parameters; interpretation is lazy to the contrary of "let ... in ...";
   hence, the "rec" keyword can be used to turn the argument of a
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 9f7491d5f..9db1c7dc4 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1609,8 +1609,8 @@ let rec xlate_vernac =
    | VernacDeclareTacticDefinition (true, tacs) ->
        (match List.map 
 	 (function
-	      ((_, id), _, body) ->
-		CT_tac_def(CT_ident (string_of_id id), xlate_tactic body))
+	      (id, _, body) ->
+		CT_tac_def(reference_to_ct_ID id, xlate_tactic body))
 	 tacs with
 	     [] -> assert false
 	   | fst::tacs1 ->
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index b7cb7fb23..46bc1a0b8 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -53,7 +53,7 @@ open Constr
 let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
 GEXTEND Gram
-  GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder_let Constr.binder subtac_nameopt;
+  GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_nameopt;
  
   subtac_gallina_loc:
     [ [ g = Vernac.gallina -> loc, g
@@ -66,9 +66,9 @@ GEXTEND Gram
     ;
 
   Constr.binder_let:
-    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> 
+    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
 	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-	    LocalRawAssum ([id], default_binder_kind, typ)
+          [LocalRawAssum ([id], default_binder_kind, typ)]
     ] ];
 
   Constr.binder:
@@ -141,7 +141,8 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
 VERNAC COMMAND EXTEND Subtac_Set_Solver
 | [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ 
     Coqlib.check_required_library ["Coq";"Program";"Tactics"];
-    Tacinterp.add_tacdef false [((dummy_loc, id_of_string "obligations_tactic"), true, t)] ]
+    Tacinterp.add_tacdef false 
+      [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d9a1d4756..fc5f4e4cb 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -187,7 +187,9 @@ is understood as
 \begin{tabular}{lcl}
 \nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
 \\
-\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr}
+\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=}
+{\tacexpr}\\
+& $|$ &{\qualid} \sequence{\ident}{} {\tt ::=}{\tacexpr}
 \end{tabular}
 \end{centerframe}
 \caption{Tactic toplevel definitions}
@@ -831,11 +833,15 @@ possible with the syntax:
 {\tacexpr}$_n$
 \end{quote}
 
-%This definition bloc is a set of definitions (use of
-%the same previous syntactical sugar) and the other scripts are evaluated as
-%usual except that the substitutions are lazily carried out (when an identifier
-%to be evaluated is the name of a recursive definition).
-
+It is also possible to \emph{redefine} an existing user-defined tactic
+using the syntax:
+\begin{quote}
+{\tt Ltac} {\qualid} {\ident}$_1$ ... {\ident}$_n$ {\tt ::=}
+{\tacexpr}
+\end{quote}
+A previous definition of \qualid must exist in the environment.
+The new definition will always be used instead of the old one and
+it goes accross module boundaries.
 
 \subsection[Printing {\ltac} tactics]{Printing {\ltac} tactics\comindex{Print Ltac}}
 
diff --git a/kernel/names.ml b/kernel/names.ml
index d1c6ee8a4..975390cb9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -320,6 +320,7 @@ type transparent_state = Idpred.t * Cpred.t
 let empty_transparent_state = (Idpred.empty, Cpred.empty)
 let full_transparent_state = (Idpred.full, Cpred.full)
 let var_full_transparent_state = (Idpred.full, Cpred.empty)
+let cst_full_transparent_state = (Idpred.empty, Cpred.full)
 
 type 'a tableKey =
   | ConstKey of constant
diff --git a/kernel/names.mli b/kernel/names.mli
index 340f6e812..b19f93e2d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -172,6 +172,7 @@ type transparent_state = Idpred.t * Cpred.t
 val empty_transparent_state : transparent_state
 val full_transparent_state : transparent_state
 val var_full_transparent_state : transparent_state
+val cst_full_transparent_state : transparent_state
 
 type inv_rel_key = int (* index in the [rel_context] part of environment
 			  starting by the end, {\em inverse} 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ea8d532f9..25a7d0b69 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -23,7 +23,7 @@ open Util
 
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
-    "end"; "as"; "let"; "dest"; "if"; "then"; "else"; "return";
+    "end"; "as"; "let"; "if"; "then"; "else"; "return";
     "Prop"; "Set"; "Type"; ".("; "_"; ".." ]
 
 let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
@@ -129,7 +129,7 @@ let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  binder binder_let binders_let delimited_binder_let delimited_binders_let
+  binder binder_let binders_let
   binders_let_fixannot typeclass_constraint pattern appl_arg;
   Constr.ident:
     [ [ id = Prim.ident -> id
@@ -210,7 +210,7 @@ GEXTEND Gram
           mkCProdN loc bl c
       | "fun"; bl = binder_list; "=>"; c = operconstr LEVEL "200" ->
           mkCLambdaN loc bl c
-      | "let"; id=name; bl = LIST0 binder_let; ty = type_cstr; ":=";
+      | "let"; id=name; bl = binders_let; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
           let loc1 = loc_of_binder_let bl in
           CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
@@ -273,13 +273,6 @@ GEXTEND Gram
     [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
         c=operconstr LEVEL "200" -> (id,fst bl,snd bl,c,ty) ] ]
   ;
-(*   fixannot: *)
-(*     [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) *)
-(*       | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel) *)
-(*       | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel) *)
-(*       | ->  (None, CStructRec) *)
-(*       ] ] *)
-(*   ; *)
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
         br=branches; "end" -> CCases(loc,RegularStyle,ty,ci,br) ] ]
@@ -340,24 +333,13 @@ GEXTEND Gram
       | s = string -> CPatPrim (loc, String s) ] ]
   ;
   binder_list:
-    [ [ idl=LIST1 name; bl=LIST0 binder_let -> 
-          LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
-      | idl=LIST1 name; ":"; c=lconstr -> 
-          [LocalRawAssum (idl,Default Explicit,c)]
-      | cl = binders_let -> cl
+    [ [ idl=LIST1 name; bl=binders_let -> 
+      LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
+    | idl=LIST1 name; ":"; c=lconstr -> 
+        [LocalRawAssum (idl,Default Explicit,c)]
+    | cl = binders_let -> cl
     ] ]
   ;
-  delimited_binders_let: 
-    [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let -> 
-	  ctx @ bl
-    | b = delimited_binder_let; cl = LIST0 binder_let -> b :: cl
-    | -> [] ] ]
-  ;
-  binders_let: 
-    [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let -> 
-	  ctx @ bl
-    | cl = LIST0 binder_let -> cl ] ]
-  ;
   binder_assum:
     [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
     | idl=LIST1 name; ":"; c=lconstr; "}" ->
@@ -379,51 +361,34 @@ GEXTEND Gram
 	(assum (loc, Name id) :: fst bl), snd bl
     | f = fixannot -> [], f
     | b = binder_let; bl = binders_let_fixannot -> 
-	b :: fst bl, snd bl
+	b @ fst bl, snd bl
     | -> [], (None, CStructRec)
     ] ]
   ;
-
+  binders_let:
+    [ [ b = binder_let; bl = binders_let -> b @ bl
+    | -> [] ] ]
+  ;
   binder_let:
     [ [ id=name ->
-          LocalRawAssum ([id],Default Explicit,CHole (loc, None))
-      | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
-          LocalRawAssum (id::idl,Default Explicit,c)
-      | "("; id=name; ":"; c=lconstr; ")" ->
-          LocalRawAssum ([id],Default Explicit,c)
-      | "{"; id=name; "}" ->
-          LocalRawAssum ([id],Default Implicit,CHole (loc, None))
-      | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
-          LocalRawAssum (id::idl,Default Implicit,c)
-      | "{"; id=name; ":"; c=lconstr; "}" ->
-          LocalRawAssum ([id],Default Implicit,c)
-      | "{"; id=name; idl=LIST1 name; "}" ->
-          LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
-      | "("; id=name; ":="; c=lconstr; ")" ->
-          LocalRawDef (id,c)
-      | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-          LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
-      | "["; tc = typeclass_constraint_binder; "]" -> tc
-    ] ]
-  ;
-  delimited_binder_let:
-    [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
-          LocalRawAssum (id::idl,Default Explicit,c)
-      | "("; id=name; ":"; c=lconstr; ")" -> 
-          LocalRawAssum ([id],Default Explicit,c)
-      | "("; id=name; ":="; c=lconstr; ")" ->
-          LocalRawDef (id,c)
-      | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
-          LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
-      | "{"; id=name; "}" ->
-          LocalRawAssum ([id],Default Implicit,CHole (loc, None))
-      | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> 
-          LocalRawAssum (id::idl,Default Implicit,c)
-      | "{"; id=name; ":"; c=lconstr; "}" -> 
-          LocalRawAssum ([id],Default Implicit,c)
-      | "{"; id=name; idl=LIST1 name; "}" -> 
-          LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
-      | "["; tc = typeclass_constraint_binder; "]" -> tc
+      [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
+    | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
+        [LocalRawAssum (id::idl,Default Explicit,c)]
+    | "("; id=name; ":"; c=lconstr; ")" -> 
+        [LocalRawAssum ([id],Default Explicit,c)]
+    | "("; id=name; ":="; c=lconstr; ")" ->
+        [LocalRawDef (id,c)]
+    | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
+        [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
+    | "{"; id=name; "}" ->
+        [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
+    | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> 
+        [LocalRawAssum (id::idl,Default Implicit,c)]
+    | "{"; id=name; ":"; c=lconstr; "}" -> 
+        [LocalRawAssum ([id],Default Implicit,c)]
+    | "{"; id=name; idl=LIST1 name; "}" -> 
+        List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
+    | "["; tc = LIST1 typeclass_constraint_binder SEP ","; "]" -> tc
     ] ]
   ;
   binder:
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index eefbe7da0..cd10e51f1 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -203,9 +203,9 @@ GEXTEND Gram
 	
   (* Definitions for tactics *)
   tacdef_body:
-    [ [ name = identref; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
+    [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
 	  (name, redef, TacFun (it, body))
-      | name = identref; redef = ltac_def_kind; body = tactic_expr ->
+      | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
 	  (name, redef, body) ] ]
   ;
   tactic:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3769d7b3e..4eafbd68c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -157,7 +157,7 @@ GEXTEND Gram
   ;
   gallina_ext:
     [ [ b = record_token; oc = opt_coercion; name = identref;
-        ps = LIST0 binder_let; 
+        ps = binders_let; 
 	s = [ ":"; s = lconstr -> s | -> CSort (loc,Rawterm.RType None) ];
 	":="; cstr = OPT identref; "{";
         fs = LIST0 record_field SEP ";"; "}" ->
@@ -237,7 +237,7 @@ GEXTEND Gram
     ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = identref; indpar = LIST0 binder_let; 
+    [ [ id = identref; indpar = binders_let; 
         c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ];
         ":="; lc = constructor_list; ntn = decl_notation ->
 	  ((id,indpar,c,lc),ntn) ] ]
@@ -258,11 +258,11 @@ GEXTEND Gram
   ;
   (* (co)-fixpoints *)
   rec_definition:
-    [ [ id = ident; b = binder_let;
+    [ [ id = ident; 
 	bl = binders_let_fixannot;
         ty = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
-	  let bl, annot = (b :: fst bl, snd bl) in
+	  let bl, annot = bl in
           let names = names_of_local_assums bl in
           let ni =
             match fst annot with
@@ -282,7 +282,7 @@ GEXTEND Gram
 	  ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = ident; bl = LIST0 binder_let; ty = type_cstr; ":=";
+    [ [ id = ident; bl = binders_let; ty = type_cstr; ":=";
         def = lconstr; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
@@ -337,10 +337,10 @@ GEXTEND Gram
         (oc,(idl,c)) ] ]
   ;
   constructor:
-    [ [ id = identref; l = LIST0 binder_let; 
+    [ [ id = identref; l = binders_let; 
         coe = of_type_with_opt_coercion; c = lconstr ->
 	  (coe,(id,mkCProdN loc l c))
-      | id = identref; l = LIST0 binder_let ->
+      | id = identref; l = binders_let ->
 	  (false,(id,mkCProdN loc l (CHole (loc, None)))) ] ]
   ;
   of_type_with_opt_coercion:
@@ -485,7 +485,7 @@ GEXTEND Gram
 	   VernacClass (qid, pars, s, [], props)
 
       (* Type classes *)
-      | IDENT "Class"; sup = OPT [ l = delimited_binders_let; "=>" -> l ];
+      | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
 	 qid = identref; pars = binders_let;
 	 s = [ ":"; c = sort -> Some (loc, c) | -> None ];
 	 props = typeclass_field_types ->
@@ -493,15 +493,20 @@ GEXTEND Gram
 	     
       | IDENT "Context"; c = typeclass_context -> 
 	  VernacContext c
-
+	    
       | global = [ IDENT "Global" -> true | -> false ];
-	 IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
-	 is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
+	 IDENT "Instance"; name = OPT identref; sup = OPT [ l = binders_let -> l ];
+(* 	 name' = OPT [ "=>"; id = identref -> id ]; *)
+	 ":" ; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
+	 pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
 	   let sup = match sup with None -> [] | Some l -> l in
 	   let is = (* We reverse the default binding mode on the right *)
-	     let n, bk, t = is in
-	       n, (match bk with Rawterm.Implicit -> Rawterm.Explicit 
-		 | Rawterm.Explicit -> Rawterm.Implicit), t 
+	     let n = 
+	       match name with
+		 | Some (loc, id) -> (loc, Name id)
+		 | None -> (dummy_loc, Anonymous)
+	     in
+	       n, expl, t 
 	   in
 	     VernacInstance (global, sup, is, props, pri)
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 481b73fd0..01b309f3c 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -442,10 +442,8 @@ module Constr =
     let lconstr_pattern = gec_constr "lconstr_pattern"
     let binder = Gram.Entry.create "constr:binder"
     let binder_let = Gram.Entry.create "constr:binder_let"
-    let delimited_binder_let = Gram.Entry.create "constr:delimited_binder_let"
     let binders_let = Gram.Entry.create "constr:binders_let"
     let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot"
-    let delimited_binders_let = Gram.Entry.create "constr:delimited_binders_let"
     let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
     let appl_arg = Gram.Entry.create "constr:appl_arg"
   end
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 6f6cff275..2525c430a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -163,11 +163,9 @@ module Constr :
     val constr_pattern : constr_expr Gram.Entry.e
     val lconstr_pattern : constr_expr Gram.Entry.e
     val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
-    val binder_let : local_binder Gram.Entry.e
-    val delimited_binder_let : local_binder Gram.Entry.e
+    val binder_let : local_binder list Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
     val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
-    val delimited_binders_let : local_binder list Gram.Entry.e
     val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
   end
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 535a4c380..bd87e09c6 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -50,7 +50,7 @@ let pr_lname = function
     (loc,Name id) -> pr_lident (loc,id)
   | lna -> pr_located pr_name lna
 
-let pr_ltac_id = Nameops.pr_id
+let pr_ltac_id = Libnames.pr_reference
 
 let pr_module = Libnames.pr_reference
 
@@ -795,13 +795,14 @@ let rec pr_vernac = function
           match body with
 	    | Tacexpr.TacFun (idl,b) -> idl,b
             | _ -> [], body in
-        pr_located pr_ltac_id id ++ 
+        pr_ltac_id id ++ 
 	prlist (function None -> str " _"
                        | Some id -> spc () ++ pr_id id) idl
 	++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
 	let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in
         pr_raw_tactic_env 
-	  (idl @ List.map snd (List.map (fun (x, _, _) -> x) l))
+	  (idl @ List.map coerce_global_to_id 
+	    (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l)))
 	  (Global.env())
 	  body in
       hov 1
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c9dee28d2..58d7e358c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2655,40 +2655,60 @@ let print_ltac id =
    errorlabstrm "print_ltac"
     (pr_qualid id ++ spc() ++ str "is not a user defined tactic")
 
+open Libnames
+
 (* Adds a definition for tactics in the table *)
-let make_absolute_name (loc,id) repl =
+let make_absolute_name ident repl =
+  let loc = loc_of_reference ident in
   try 
-    let kn = if repl then Nametab.locate_tactic (make_short_qualid id) else Lib.make_kn id in
+    let id, kn = 
+      if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident))
+      else let id = Pcoq.coerce_global_to_id ident in
+	     Some id, Lib.make_kn id 
+    in
       if Gmap.mem kn !mactab then
-	if repl then kn
+	if repl then id, kn
 	else
 	  user_err_loc (loc,"Tacinterp.add_tacdef",
-		       str "There is already an Ltac named " ++ pr_id id)
+		       str "There is already an Ltac named " ++ pr_reference ident)
       else if is_atomic_kn kn then 
 	user_err_loc (loc,"Tacinterp.add_tacdef",
-		     str "Reserved Ltac name " ++ pr_id id)
-      else kn
+		     str "Reserved Ltac name " ++ pr_reference ident)
+      else id, kn
   with Not_found ->
     user_err_loc (loc,"Tacinterp.add_tacdef",
-		 str "There is no Ltac named " ++ pr_id id)
+		 str "There is no Ltac named " ++ pr_reference ident)
+
+let rec filter_map f l = 
+  let rec aux acc = function
+      [] -> acc
+    | hd :: tl -> 
+	match f hd with
+	    Some x -> aux (x :: acc) tl
+	  | None -> aux acc tl
+  in aux [] l
       
 let add_tacdef isrec tacl =
-(*  let isrec = if !Flags.p1 then isrec else true in*)
-  let rfun = List.map (fun ((loc,id as locid),b,_) -> (id,make_absolute_name locid b)) tacl in
+  let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
   let ist =
-    {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in
+    {(make_empty_glob_sign()) with ltacrecvars = 
+	if isrec then filter_map 
+	  (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun 
+	else []} in
   let gtacl =
-    List.map2 (fun ((_,id),b,def) (_, qid) ->
-      let k = if b then UpdateTac qid else NewTac id in
+    List.map2 (fun (_,b,def) (id, qid) ->
+      let k = if b then UpdateTac qid else NewTac (Option.get id) in
       let t = Flags.with_option strict_check (intern_tactic ist) def in
 	(k, t))
       tacl rfun in
   let id0 = fst (List.hd rfun) in
-  let _ = Lib.add_leaf id0 (inMD gtacl) in
+  let _ = match id0 with Some id0 -> ignore(Lib.add_leaf id0 (inMD gtacl))
+    | _ -> Lib.add_anonymous_leaf (inMD gtacl) in
   List.iter
-    (fun ((_,id),b,_) -> 
-      if b then Flags.if_verbose msgnl (pr_id id ++ str " is redefined")
-      else Flags.if_verbose msgnl (pr_id id ++ str " is defined"))
+    (fun (id,b,_) -> 
+      Flags.if_verbose msgnl (Libnames.pr_reference id ++ 
+				 (if b then str " is redefined"
+				   else str " is defined")))
     tacl
 
 (***************************************************************************)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index db67d1473..2a490fdac 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -63,7 +63,7 @@ val get_debug : unit -> debug_info
 
 (* Adds a definition for tactics in the table *)
 val add_tacdef :
-  bool -> (identifier Util.located * bool * raw_tactic_expr) list -> unit
+  bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit
 val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
 (* Tactic extensions *)
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 62744b1d1..d96a532c3 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -94,8 +94,8 @@ Program Instance unit_eqdec : ! EqDec unit eq :=
     reflexivity.
   Qed.
 
-Program Instance [ EqDec A eq, EqDec B eq ] => 
-  prod_eqdec : ! EqDec (prod A B) eq :=
+Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] :
+  ! EqDec (prod A B) eq :=
   equiv_dec x y := 
     let '(x1, x2) := x in 
     let '(y1, y2) := y in 
@@ -106,8 +106,8 @@ Program Instance [ EqDec A eq, EqDec B eq ] =>
 
   Solve Obligations using unfold complement, equiv ; program_simpl.
 
-Program Instance [ EqDec A eq, EqDec B eq ] => 
-  sum_eqdec : ! EqDec (sum A B) eq :=
+Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] :
+  ! EqDec (sum A B) eq :=
   equiv_dec x y := 
     match x, y with
       | inl a, inl b => if a == b then in_left else in_right
@@ -121,7 +121,7 @@ Program Instance [ EqDec A eq, EqDec B eq ] =>
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq :=
+Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then in_left
@@ -138,7 +138,7 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq
 
 Require Import List.
 
-Program Instance [ eqa : EqDec A eq ] => list_eqdec : ! EqDec (list A) eq :=
+Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq :=
   equiv_dec := 
     fix aux (x : list A) y { struct x } :=
     match x, y with
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 23af8a744..42961baea 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -52,16 +52,16 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
 (** Shortcuts to make proof search easier. *)
 
-Program Instance [ sa : Equivalence A ] => equiv_reflexive : Reflexive equiv.
+Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv.
 
-Program Instance [ sa : Equivalence A ] => equiv_symmetric : Symmetric equiv.
+Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv.
 
   Next Obligation.
   Proof.
     symmetry ; auto.
   Qed.
 
-Program Instance [ sa : Equivalence A ] => equiv_transitive : Transitive equiv.
+Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv.
 
   Next Obligation.
   Proof.
@@ -116,8 +116,8 @@ Section Respecting.
   Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
     { morph : A -> B | respectful R R' morph morph }.
   
-  Program Instance [ Equivalence A R, Equivalence B R' ] => 
-    respecting_equiv : Equivalence respecting
+  Program Instance respecting_equiv [ Equivalence A R, Equivalence B R' ] :
+    Equivalence respecting
     (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
 
   Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
@@ -134,8 +134,8 @@ End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance [ Equivalence A eqA ] => 
-  pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA) | 9.
+Program Instance pointwise_equivalence [ Equivalence A eqA ] :
+  Equivalence (B -> A) (pointwise_relation eqA) | 9.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 5ac6d8ee5..cd38f318c 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -87,12 +87,12 @@ Proof. firstorder. Qed.
 
 (** The subrelation property goes through products as usual. *)
 
-Instance [ sub : subrelation A R₁ R₂ ] =>
-  morphisms_subrelation : ! subrelation (B -> A) (R ==> R₁) (R ==> R₂).
+Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] :
+  ! subrelation (B -> A) (R ==> R₁) (R ==> R₂).
 Proof. firstorder. Qed.
 
-Instance [ sub : subrelation A R₂ R₁ ] =>
-  morphisms_subrelation_left : ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
+Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] :
+  ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
 Proof. firstorder. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
@@ -129,16 +129,15 @@ Proof. firstorder. Qed.
 Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
 Proof. firstorder. Qed.
 
-Instance [ sub : subrelation A R R' ] => pointwise_subrelation :
+Instance pointwise_subrelation [ sub : subrelation A R R' ] :
   subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4.
 Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
 
 (** The complement of a relation conserves its morphisms. *)
 
-Program Instance [ mR : Morphism (A -> A -> Prop)
-  (RA ==> RA ==> iff) R ] => 
-  complement_morphism : Morphism (RA ==> RA ==> iff)
-  (complement R).
+Program Instance complement_morphism
+  [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] :
+  Morphism (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
   Proof.
@@ -149,8 +148,9 @@ Program Instance [ mR : Morphism (A -> A -> Prop)
 
 (** The [inverse] too, actually the [flip] instance is a bit more general. *) 
 
-Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => 
-  flip_morphism : Morphism (RB ==> RA ==> RC) (flip f).
+Program Instance flip_morphism
+  [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] :
+  Morphism (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
   Proof.
@@ -160,8 +160,8 @@ Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] =>
 (** Every Transitive relation gives rise to a binary morphism on [impl], 
    contravariant in the first argument, covariant in the second. *)
 
-Program Instance [ Transitive A R ] => 
-  trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
+Program Instance trans_contra_co_morphism
+  [ Transitive A R ] : Morphism (R --> R ++> impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -181,40 +181,40 @@ Program Instance [ Transitive A R ] =>
 
 (** Morphism declarations for partial applications. *)
 
-Program Instance [ Transitive A R ] =>
-  trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
+Program Instance trans_contra_inv_impl_morphism
+  [ Transitive A R ] : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-Program Instance [ Transitive A R ] =>
-  trans_co_impl_morphism : Morphism (R ==> impl) (R x).
+Program Instance trans_co_impl_morphism
+  [ Transitive A R ] : Morphism (R ==> impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity x0...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric A R ] =>
-  trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
+Program Instance trans_sym_co_inv_impl_morphism
+  [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric _ R ] =>
-  trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
+Program Instance trans_sym_contra_impl_morphism
+  [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity x0...
   Qed.
 
-Program Instance [ Equivalence A R ] =>
-  equivalence_partial_app_morphism : Morphism (R ==> iff) (R x).
+Program Instance equivalence_partial_app_morphism
+  [ Equivalence A R ] : Morphism (R ==> iff) (R x).
 
   Next Obligation.
   Proof with auto.
@@ -227,8 +227,8 @@ Program Instance [ Equivalence A R ] =>
 (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
    to get an [R y z] goal. *)
 
-Program Instance [ Transitive A R ] => 
-  trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
+Program Instance trans_co_eq_inv_impl_morphism
+  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -245,8 +245,8 @@ Program Instance [ Transitive A R ] =>
 
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ Transitive A R, Symmetric _ R ] => 
-  trans_sym_morphism : Morphism (R ==> R ==> iff) R.
+Program Instance trans_sym_morphism
+  [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
   Proof with auto.
@@ -256,8 +256,8 @@ Program Instance [ Transitive A R, Symmetric _ R ] =>
     transitivity y... transitivity y0... 
   Qed.
 
-Program Instance [ Equivalence A R ] =>
-  equiv_morphism : Morphism (R ==> R ==> iff) R.
+Program Instance equiv_morphism [ Equivalence A R ] :
+  Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
   Proof with auto.
@@ -288,7 +288,7 @@ Program Instance inverse_iff_impl_id :
 (*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
 (* Proof. simpl_relation. Qed. *)
 
-Instance (A : Type) [ Reflexive B R' ] =>
+Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] :
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
@@ -322,12 +322,12 @@ Qed.
 Class MorphismProxy A (R : relation A) (m : A) : Prop :=
   respect_proxy : R m m.
 
-Instance [ Reflexive A R ] (x : A) => 
-  reflexive_morphism_proxy : MorphismProxy A R x | 1.
+Instance reflexive_morphism_proxy
+  [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1.
 Proof. firstorder. Qed.
 
-Instance [ Morphism A R x ] =>
-  morphism_morphism_proxy : MorphismProxy A R x | 2.
+Instance morphism_morphism_proxy
+  [ Morphism A R x ] : MorphismProxy A R x | 2.
 Proof. firstorder. Qed.
 
 (* Instance (A : Type) [ Reflexive B R ] => *)
@@ -392,8 +392,8 @@ Instance not_inverse_respectful_norm :
   Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
 Proof. firstorder. Qed.
 
-Instance [ Normalizes B R' (inverse R'') ] =>
-  inverse_respectful_rec_norm : Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
+Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] :
+  Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
 Proof. red ; intros.  
   pose normalizes as r.
   setoid_rewrite r.
@@ -403,8 +403,8 @@ Qed.
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)
 
-Program Instance [ Morphism A R m ] => 
-  morphism_inverse_morphism : Morphism (inverse R) m | 2.
+Program Instance morphism_inverse_morphism
+  [ Morphism A R m ] : Morphism (inverse R) m | 2.
 
 (** Bootstrap !!! *)
 
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 301fba534..7dc1f95ef 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -73,7 +73,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl
 
 (** Morphisms for quantifiers *)
 
-Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A).
+Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation iff ==> iff) (@ex A).
 
   Next Obligation.
   Proof.
@@ -86,7 +86,7 @@ Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation if
     exists x₁. rewrite H. assumption.
   Qed.
 
-Program Instance {A : Type} => ex_impl_morphism :
+Program Instance ex_impl_morphism {A : Type} :
   Morphism (pointwise_relation impl ==> impl) (@ex A).
 
   Next Obligation.
@@ -95,7 +95,7 @@ Program Instance {A : Type} => ex_impl_morphism :
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance {A : Type} => ex_inverse_impl_morphism : 
+Program Instance ex_inverse_impl_morphism {A : Type} : 
   Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A).
 
   Next Obligation.
@@ -104,7 +104,7 @@ Program Instance {A : Type} => ex_inverse_impl_morphism :
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance {A : Type} => all_iff_morphism : 
+Program Instance all_iff_morphism {A : Type} : 
   Morphism (pointwise_relation iff ==> iff) (@all A).
 
   Next Obligation.
@@ -113,7 +113,7 @@ Program Instance {A : Type} => all_iff_morphism :
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance {A : Type} => all_impl_morphism : 
+Program Instance all_impl_morphism {A : Type} : 
   Morphism (pointwise_relation impl ==> impl) (@all A).
   
   Next Obligation.
@@ -122,7 +122,7 @@ Program Instance {A : Type} => all_impl_morphism :
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance {A : Type} => all_inverse_impl_morphism : 
+Program Instance all_inverse_impl_morphism {A : Type} : 
   Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A).
   
   Next Obligation.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 015eb7323..25316c278 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -65,26 +65,26 @@ Unset Implicit Arguments.
 
 (** We can already dualize all these properties. *)
 
-Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
+Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) :=
   reflexivity := reflexivity (R:=R).
 
-Program Instance [ Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) :=
+Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) :=
   irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ Symmetric A R ] => flip_Symmetric : Symmetric (flip R).
+Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric.
 
-Program Instance [ Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R).
+Program Instance flip_Asymmetric [ Asymmetric A R ] : Asymmetric (flip R).
   
   Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R).
+Program Instance flip_Transitive [ Transitive A R ] : Transitive (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
 
-Program Instance [ Reflexive A (R : relation A) ] => 
-  Reflexive_complement_Irreflexive : Irreflexive (complement R).
+Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ]
+   : Irreflexive (complement R).
 
   Next Obligation. 
   Proof. 
@@ -95,7 +95,7 @@ Program Instance [ Reflexive A (R : relation A) ] =>
   Qed.
 
 
-Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R).
+Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R).
 
   Next Obligation.
   Proof.
@@ -165,8 +165,7 @@ Class PER (carrier : Type) (pequiv : relation carrier) : Prop :=
 (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
 
-Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => 
-  arrow_per : PER (A -> B)
+Program Instance arrow_per [ PER A (R : relation A), PER B (R' : relation B) ] : PER (A -> B)
   (fun f g => forall (x y : A), R x y -> R' (f x) (g y)).
 
   Next Obligation.
@@ -188,8 +187,8 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop :=
 Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
   antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
-Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq R ] => 
-  flip_antiSymmetric : Antisymmetric eq (flip R).
+Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] :
+  Antisymmetric eq (flip R).
 
 (** Leibinz equality [eq] is an equivalence relation.
    The instance has low priority as it is always applicable 
@@ -368,7 +367,7 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio
 
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
-Instance (A : Type) => relation_equivalence_equivalence :
+Instance relation_equivalence_equivalence (A : Type) :
   Equivalence (relation A) relation_equivalence.
 Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
 
@@ -387,7 +386,7 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
    for equivalence (see Morphisms).
    It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
 
-Instance [ PartialOrder A eqA R ] =>  partial_order_antisym : ! Antisymmetric A eqA R.
+Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA R.
 Proof with auto.
   reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. 
   apply <- poe. firstorder.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 639b15f50..4d6601a6e 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -95,8 +95,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] => 
-  prod_eqdec : EqDec (@eq_setoid (prod A B)) :=
+Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : EqDec (@eq_setoid (prod A B)) :=
   equiv_dec x y := 
     let '(x1, x2) := x in 
     let '(y1, y2) := y in 
@@ -111,7 +110,7 @@ Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] =>
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance [ ! EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
+Program Instance bool_function_eqdec [ ! EqDec (@eq_setoid A) ] : EqDec (@eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then in_left
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 8412cc102..aeaa197e8 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -38,8 +38,7 @@ Definition default_relation [ DefaultRelation A R ] := R.
 
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
-Instance [ Equivalence A R ] => 
-  equivalence_default : DefaultRelation A R | 4.
+Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4.
 
 (** The setoid_replace tactics in Ltac, defined in terms of default relations and
    the setoid_rewrite tactic. *)
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 8ce84c827..c9de1a9e1 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -9,7 +9,7 @@
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
 
-Open Local Scope subset_scope.
+Open Local Scope program_scope.
 
 (** Tactics related to subsets and proof irrelevance. *)
 
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 6158e88f7..6cd75257b 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(* -*- coq-prog-args: ("-emacs-U") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -13,10 +13,6 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(** Unicode lambda abstraction, does not work with factorization of lambdas. *)
-
-Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T at level 10, y at next level, no associativity) : program_scope.
-
 (** Notations for the unit type and value. *)
 
 Notation " () " := Datatypes.unit : type_scope.
@@ -42,11 +38,11 @@ Implicit Arguments cons [[A]].
 
 (** Standard notations for lists. *)
 
-Notation " [] " := nil.
-Notation " [ x ] " := (cons x nil).
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1).
+Notation " [ ] " := nil : list_scope.
+Notation " [ x ] " := (cons x nil) : list_scope.
+Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
 
-(** n-ary exists ! *)
+(** n-ary exists *)
 
 Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
   (at level 200, x ident, y ident, right associativity) : type_scope.
@@ -61,9 +57,3 @@ Tactic Notation "exist" constr(x) := exists x.
 Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
 Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
 Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
-
-(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *)
-(*   (at level 200, x ident, y ident, right associativity) : program_scope. *)
-
-(* Notation " 'Π' x : T , p " := (forall x : T, p) *)
-(*   (at level 200, x ident, right associativity) : program_scope. *)
\ No newline at end of file
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 23f0a7d38..c4a20506c 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -12,18 +12,12 @@ Require Export Coq.Program.Tactics.
 
 Set Implicit Arguments.
 
-(** Wrap a proposition inside a subset. *)
-
-Notation " {{ x }} " := (tt : { y : unit | x }).
-
 (** A simpler notation for subsets defined on a cartesian product. *)
 
 Notation "{ ( x , y )  :  A  |  P }" :=
   (sig (fun anonymous : A => let (x,y) := anonymous in P))
   (x ident, y ident, at level 10) : type_scope.
 
-(** The scope in which programs are typed (not their types). *)
-
 (** Generates an obligation to prove False. *)
 
 Notation " ! " := (False_rect _ _) : program_scope.
@@ -32,19 +26,12 @@ Delimit Scope program_scope with prg.
 
 (** Abbreviation for first projection and hiding of proofs of subset objects. *)
 
-Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : subset_scope.
-
-Delimit Scope subset_scope with subset.
-
-(* In [subset_scope] to allow masking by redefinitions for particular types. *)
-Notation "( x & ? )" := (@exist _ _ x _) : subset_scope.
+Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope.
 
 (** Coerces objects to their support before comparing them. *)
 
 Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope.
 
-(** Quantifying over subsets. *)
-
 Require Import Coq.Bool.Sumbool.
 
 (** Construct a dependent disjunction from a boolean. *)
@@ -59,10 +46,11 @@ Notation "'in_left'" := (@left _ _ _) : program_scope.
 Notation "'in_right'" := (@right _ _ _) : program_scope.
 
 (** Extraction directives *)
-
+(*
 Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
 (* Extract Inductive sigT => "prod" [ "" ]. *)
+*)
\ No newline at end of file
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 20dfe9b01..d24312ff1 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -2,7 +2,7 @@ Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
 Require Import ProofIrrelevance.
 
-Open Local Scope subset_scope.
+Open Local Scope program_scope.
 
 Implicit Arguments Enriching Acc_inv [y].
 
@@ -91,9 +91,9 @@ Section Well_founded_measure.
     
     Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
     
-    Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
-      F_sub x (fun y: { y : A | m y < m x}  => Fix_measure_F_sub (proj1_sig y) 
-        (@Acc_inv _ _ _ r (m (proj1_sig y)) (proj2_sig y))).
+    Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
+      F_sub x (fun (y : A | m y < m x)  => Fix_measure_F_sub y
+        (@Acc_inv _ _ _ r (m y) (proj2_sig y))).
     
     Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
   
@@ -102,7 +102,7 @@ Section Well_founded_measure.
   Section FixPoint.
     Variable P : A -> Type.
     
-    Variable F_sub : forall x:A, (forall (y : A | m y < m x), P (proj1_sig y)) -> P x.
+    Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x.
     
     Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
     
@@ -113,9 +113,9 @@ Section Well_founded_measure.
       forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)),
         (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
 
-    Lemma Fix_measure_F_eq :
+    Program Lemma Fix_measure_F_eq :
       forall (x:A) (r:Acc lt (m x)),
-        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r.
+        F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r.
     Proof.
       intros x.
       set (y := m x).
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 22430b7ed..16589805f 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -286,7 +286,7 @@ type vernac_expr =
 
   (* Commands *)
   | VernacDeclareTacticDefinition of
-      rec_flag * (lident * bool * raw_tactic_expr) list
+      rec_flag * (reference * bool * raw_tactic_expr) list
   | VernacHints of locality_flag * lstring list * hints
   | VernacSyntacticDefinition of identifier * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag