Merge branch 'v8.5'

22 files changed, 224 insertions, 82 deletions

diff --git a/Makefile.doc b/Makefile.doc
index bc6ae020b1..33dd60dbad 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -53,7 +53,7 @@ ifdef QUICK
 %.v.tex: %.tex
 	$(COQTEX) $(COQTEXOPTS) $<
 else
-%.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO)
+%.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(ALLVO)
 	$(COQTEX) $(COQTEXOPTS) $<
 endif
 
@@ -202,12 +202,12 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
 ifdef QUICK
 doc/stdlib/html/genindex.html:
 else
-doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO)
+doc/stdlib/html/genindex.html: | $(COQDOC) $(ALLVO)
 endif
 	- rm -rf doc/stdlib/html
 	$(MKDIR) doc/stdlib/html
 	$(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \
-	  -R theories Coq $(THEORIESVO:.vo=.v)
+	  -R theories Coq -R plugins Coq $(VFILES)
 	mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html
 
 doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
@@ -246,12 +246,12 @@ doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex
 ifdef QUICK
 doc/stdlib/FullLibrary.coqdoc.tex:
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
-            -R theories Coq $(THEORIESVO:.vo=.v) > $@
+            -R theories Coq -R plugins Coq $(VFILES) > $@
 	sed -i.tmp -e 's///g' $@ && rm $@.tmp
 else
-doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(THEORIESVO)
+doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(ALLVO)
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
-            -R theories Coq $(THEORIESVO:.vo=.v) > $@
+            -R theories Coq -R plugins Coq $(VFILES) > $@
 	sed -i.tmp -e 's///g' $@ && rm $@.tmp
 endif
 
diff --git a/checker/univ.ml b/checker/univ.ml
index 5fed6dcd5a..3bcb3bc950 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -174,6 +174,16 @@ struct
     | _, Level _ -> 1
     | Var n, Var m -> Int.compare n m
 
+  let hequal x y =
+    x == y ||
+      match x, y with
+      | Prop, Prop -> true
+      | Set, Set -> true
+      | Level (n,d), Level (n',d') ->
+        n == n' && d == d'
+      | Var n, Var n' -> n == n'
+      | _ -> false
+
   let hcons = function
     | Prop as x -> x
     | Set as x -> x
@@ -211,27 +221,26 @@ module Level = struct
 
   let hash x = x.hash
 
-  let hcons x = 
-    let data' = RawLevel.hcons x.data in
-      if data' == x.data then x
-      else { x with data = data' }
-
   let data x = x.data
 
   (** Hashcons on levels + their hash *)
 
-  let make =
-    let module Self = struct
-      type _t = t
-      type t = _t
-      let equal = equal
-      let hash = hash
-    end in
-    let module WH = Weak.Make(Self) in
-    let pool = WH.create 4910 in fun x ->
-    let x = { hash = RawLevel.hash x; data = x } in
-    try WH.find pool x
-    with Not_found -> WH.add pool x; x
+  module Self = struct
+    type _t = t
+    type t = _t
+    type u = unit
+    let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+    let hash x = x.hash
+    let hashcons () x =
+      let data' = RawLevel.hcons x.data in
+      if x.data == data' then x else { x with data = data' }
+  end
+
+  let hcons =
+    let module H = Hashcons.Make(Self) in
+    Hashcons.simple_hcons H.generate H.hcons ()
+
+  let make l = hcons { hash = RawLevel.hash l; data = l }
 
   let set = make Set
   let prop = make Prop
diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex
index 696fff4f74..bb4c5ce469 100644
--- a/doc/whodidwhat/whodidwhat-8.4update.tex
+++ b/doc/whodidwhat/whodidwhat-8.4update.tex
@@ -3,6 +3,7 @@
 \usepackage{fullpage}
 \usepackage[utf8]{inputenc}
 \usepackage{t1enc}
+\usepackage{hyperref}
 
 \begin{document}
 
@@ -32,7 +33,7 @@
   \end{itemize}
 \item The universe hierarchy
   \begin{itemize}
-  \item Floating universes: Gérard Huet, with contributions from Bruno Barras
+  \item Floating universes: Gérard Huet, with contributions from Bruno Barras and Pierre Letouzey
   \item Algebraic universes: Hugo Herbelin
   \end{itemize}
 \item Mutual inductive types and recursive definitions
@@ -296,10 +297,15 @@
 \section{Maintenance and system engineering}
 
 \begin{itemize}
-\item General bug support: Gérard Huet, Christine Paulin, Chet Murthy,
-  Jean-Christophe Filliâtre, Hugo Herbelin, Bruno Barras, Pierre
-  Letouzey with contributions at some time from Benjamin Werner,
-  Jean-Marc Notin, Pierre Boutillier, ...
+%\item General maintenance in version 8.0: Bruno Barras, Hugo Herbelin
+%\item General maintenance in version 8.1: Bruno Barras, Hugo Herbelin, Jean-Marc Notin
+%\item General maintenance in version 8.2: Hugo Herbelin, Pierre Letouzey, Jean-Marc Notin, 
+%\item General maintenance in version 8.3: Hugo Herbelin, Pierre
+%  Letouzey
+\item General maintenance in version 8.4: Pierre Letouzey, Hugo
+  Herbelin, Pierre Boutillier, Matthieu Sozeau, Stéphane Glondu with
+  contributions from Guillaume Melquiond, Julien Narboux and
+  Pierre-Marie Pédrot
 \item Team coordination: Gérard Huet, Christine Paulin, Hugo Herbelin,
   with various other contributions
 \item Packaging tools: Henri Laulhere, David Delahaye, Julien Narboux,
@@ -327,8 +333,10 @@
 \begin{itemize}
 \item Searching modulo isomorphism: David Delahaye
 \item Explanation of proofs in pseudo-natural language: Yann Coscoy
+\item Dp: Jean-Christophe Filliâtre, Nicolas Ayache with contributions
+  from Claude Marché (now integrated to \href{http://why3.lri.fr/}{Why3})
 \end{itemize}
 
-For probable oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr
+For oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr
 
 \end{document}
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index f4b81a241b..dc52ea9aad 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -327,14 +327,14 @@ let handle_exn (e, info) =
   let loc_of e = match Loc.get_loc e with
     | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
     | _ -> None in
-  let mk_msg e = read_stdout ()^"\n"^string_of_ppcmds (Errors.print e) in
+  let mk_msg () = read_stdout ()^"\n"^string_of_ppcmds (Errors.print ~info e) in
   match e with
   | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!"
   | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!"
   | e ->
       match Stateid.get info with
-      | Some (valid, _) -> valid, loc_of info, mk_msg e
-      | None -> dummy, loc_of info, mk_msg e
+      | Some (valid, _) -> valid, loc_of info, mk_msg ()
+      | None -> dummy, loc_of info, mk_msg ()
 
 let init =
   let initialized = ref false in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 2642b1867d..48dbacf1a4 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -153,13 +153,13 @@ let type_of_constant_type_knowing_parameters env t paramtyps =
 
 let type_of_constant_knowing_parameters env cst paramtyps =
   let cb = lookup_constant (fst cst) env in
-  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ty, cu = constant_type env cst in
     type_of_constant_type_knowing_parameters env ty paramtyps, cu
 
 let type_of_constant_knowing_parameters_in env cst paramtyps =
   let cb = lookup_constant (fst cst) env in
-  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ty = constant_type_in env cst in
     type_of_constant_type_knowing_parameters env ty paramtyps
 
@@ -171,14 +171,14 @@ let type_of_constant env cst =
 
 let type_of_constant_in env cst =
   let cb = lookup_constant (fst cst) env in
-  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ar = constant_type_in env cst in
     type_of_constant_type_knowing_parameters env ar [||]
 
 let judge_of_constant_knowing_parameters env (kn,u as cst) args =
   let c = mkConstU cst in
   let ty, cu = type_of_constant_knowing_parameters env cst args in
-  let _ = Environ.check_constraints cu env in
+  let () = check_constraints cu env in
     make_judge c ty
 
 let judge_of_constant env cst =
@@ -372,7 +372,7 @@ let judge_of_case env ci pj cj lfj =
   let (pind, _ as indspec) =
     try find_rectype env cj.uj_type
     with Not_found -> error_case_not_inductive env cj in
-  let _ = check_case_info env pind ci in
+  let () = check_case_info env pind ci in
   let (bty,rslty) =
     type_case_branches env indspec pj cj.uj_val in
   let () = check_branch_types env pind cj (lfj,bty) in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 492762df39..763c0822f2 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -194,7 +194,17 @@ struct
     | Level _, _ -> -1
     | _, Level _ -> 1
     | Var n, Var m -> Int.compare n m
-      
+
+  let hequal x y =
+    x == y ||
+      match x, y with
+      | Prop, Prop -> true
+      | Set, Set -> true
+      | Level (n,d), Level (n',d') ->
+        n == n' && d == d'
+      | Var n, Var n' -> n == n'
+      | _ -> false
+
   let hcons = function
     | Prop as x -> x
     | Set as x -> x
@@ -233,27 +243,26 @@ module Level = struct
 
   let hash x = x.hash
 
-  let hcons x = 
-    let data' = RawLevel.hcons x.data in
-      if data' == x.data then x
-      else { x with data = data' }
-
   let data x = x.data
 
   (** Hashcons on levels + their hash *)
 
-  let make =
-    let module Self = struct
-      type _t = t
-      type t = _t
-      let equal = equal
-      let hash = hash
-    end in
-    let module WH = Weak.Make(Self) in
-    let pool = WH.create 4910 in fun x ->
-    let x = { hash = RawLevel.hash x; data = x } in
-    try WH.find pool x
-    with Not_found -> WH.add pool x; x
+  module Self = struct
+    type _t = t
+    type t = _t
+    type u = unit
+    let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+    let hash x = x.hash
+    let hashcons () x =
+      let data' = RawLevel.hcons x.data in
+      if x.data == data' then x else { x with data = data' }
+  end
+
+  let hcons =
+    let module H = Hashcons.Make(Self) in
+    Hashcons.simple_hcons H.generate H.hcons ()
+
+  let make l = hcons { hash = RawLevel.hash l; data = l }
 
   let set = make Set
   let prop = make Prop
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 752e2634a6..46ba0b6285 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -43,6 +43,7 @@ module type S =
     type table
     val generate : u -> table
     val hcons : table -> t -> t
+    val stats : table -> Hashset.statistics
   end
 
 module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
@@ -67,6 +68,8 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
       let y = X.hashcons u x in
       Htbl.repr (X.hash y) y tab
 
+    let stats (tab, _) = Htbl.stats tab
+
   end
 
 (* A few usefull wrappers:
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 60a9ee01c1..8d0adc3fd6 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -56,6 +56,8 @@ module type S =
     (** This create a hashtable of the hashconsed objects. *)
     val hcons : table -> t -> t
     (** Perform the hashconsing of the given object within the table. *)
+    val stats : table -> Hashset.statistics
+    (** Recover statistics of the hashconsing table. *)
   end
 
 module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u)
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 6bec81c756..1ca6cc6418 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -19,12 +19,20 @@ module type EqType = sig
   val equal : t -> t -> bool
 end
 
+type statistics = {
+  num_bindings: int;
+  num_buckets: int;
+  max_bucket_length: int;
+  bucket_histogram: int array
+}
+
 module type S = sig
   type elt
   type t
   val create : int -> t
   val clear : t -> unit
   val repr : int -> elt -> t -> elt
+  val stats : t -> statistics
 end
 
 module Make (E : EqType) =
@@ -185,6 +193,24 @@ module Make (E : EqType) =
     let ifnotfound index = add_aux t Weak.set (Some d) h index; d in
     find_or h t d ifnotfound
 
+  let stats t =
+    let fold accu bucket = max (count_bucket 0 bucket 0) accu in
+    let max_length = Array.fold_left fold 0 t.table in
+    let histogram = Array.make (max_length + 1) 0 in
+    let iter bucket =
+      let len = count_bucket 0 bucket 0 in
+      histogram.(len) <- succ histogram.(len)
+    in
+    let () = Array.iter iter t.table in
+    let fold (num, len, i) k = (num + k * i, len + k, succ i) in
+    let (num, len, _) = Array.fold_left fold (0, 0, 0) histogram in
+    {
+      num_bindings = num;
+      num_buckets = len;
+      max_bucket_length = Array.length histogram;
+      bucket_histogram = histogram;
+    }
+
 end
 
 module Combine = struct
diff --git a/lib/hashset.mli b/lib/hashset.mli
index 537f3418e4..a455eec662 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -19,6 +19,13 @@ module type EqType = sig
   val equal : t -> t -> bool
 end
 
+type statistics = {
+  num_bindings: int;
+  num_buckets: int;
+  max_bucket_length: int;
+  bucket_histogram: int array
+}
+
 module type S = sig
   type elt
   (** Type of hashsets elements. *)
@@ -34,6 +41,8 @@ module type S = sig
       specific representation that is stored in [set]. Otherwise,
       [constr] is stored in [set] and will be used as the canonical
       representation of this value in the future. *)
+  val stats : t -> statistics
+  (** Recover statistics on the table. *)
 end
 
 module Make (E : EqType) : S with type elt = E.t
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fdb19d3780..7c3165fa8e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1644,7 +1644,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
   in
   aux (0,extenv,subst0) t0
 
-let build_tycon loc env tycon_env subst tycon extenv evdref t =
+let build_tycon loc env tycon_env s subst tycon extenv evdref t =
   let t,tt = match t with
     | None ->
 	(* This is the situation we are building a return predicate and
@@ -1659,6 +1659,8 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
         let evd,tt = Typing.e_type_of extenv !evdref t in
         evdref := evd;
         (t,tt) in
+  let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
+  if not b then anomaly (Pp.str "Build_tycon: should be a type");
   { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
@@ -1780,7 +1782,7 @@ let build_inversion_problem loc env sigma tms t =
       mat       = [eqn1;eqn2];
       caseloc   = loc;
       casestyle = RegularStyle;
-      typing_function = build_tycon loc env pb_env subst} in
+      typing_function = build_tycon loc env pb_env s subst} in
   let pred = (compile pb).uj_val in
   (!evdref,pred)
 
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index a6e2bc19db..cf6ac619dd 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -441,7 +441,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
 	try 
 	  let term = Retyping.expand_projection env sigma p c' [] in
 	    aux env term mk_ctx next
-	with Retyping.RetypeError _ -> raise PatternMatchingFailure
+	with Retyping.RetypeError _ -> next ()
       else
 	try_aux [env] [c'] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
diff --git a/stm/stm.ml b/stm/stm.ml
index 3a57d85bab..96a11d306d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2278,7 +2278,7 @@ let interp verb (_,e as lexpr) =
     let print_goals =
       verb && match clas with
        | VtQuery _, _ -> false
-       | (VtProofStep _ | VtStm (VtBack _, _)), _ -> true
+       | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
        | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in
     try finish ~print_goals ()
     with e ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a96ae26888..9265328a47 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1958,21 +1958,25 @@ let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented")
 let declare_intro_decomp_eq f = intro_decomp_eq_function := f
 
 let my_find_eq_data_decompose gl t =
-  try find_eq_data_decompose gl t
+  try Some (find_eq_data_decompose gl t)
   with e when is_anomaly e
     (* Hack in case equality is not yet defined... one day, maybe,
        known equalities will be dynamically registered *)
-      -> raise Constr_matching.PatternMatchingFailure
+      -> None
+  | Constr_matching.PatternMatchingFailure -> None
 
 let intro_decomp_eq loc l thin tac id =
   Proofview.Goal.nf_enter begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_type_of gl c in
   let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
-  let eq,u,eq_args = my_find_eq_data_decompose gl t in
-  !intro_decomp_eq_function
+  match my_find_eq_data_decompose gl t with
+  | Some (eq,u,eq_args) ->
+    !intro_decomp_eq_function
     (fun n -> tac ((dloc,id)::thin) (Some (true,n)) l)
     (eq,t,eq_args) (c, t)
+  | None ->
+    Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
   end
 
 let intro_or_and_pattern loc bracketed ll thin tac id =
diff --git a/test-suite/bugs/closed/3900.v b/test-suite/bugs/closed/3900.v
new file mode 100644
index 0000000000..6be2161c2f
--- /dev/null
+++ b/test-suite/bugs/closed/3900.v
@@ -0,0 +1,13 @@
+Global Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Variable A : PreCategory.
+Variable Pobj : A -> Type.
+Local Notation obj := (sigT Pobj).
+Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type.
+Class Foo (x : Type) := { _ : forall y, y }.
+Local Instance ishset_pmor {s d m} : Foo (Pmor s d m).
+Proof.
+SearchAbout ((forall _ _, _) -> Foo _).
+Abort.
diff --git a/test-suite/bugs/closed/4001.v b/test-suite/bugs/closed/4001.v
new file mode 100644
index 0000000000..25d78f4b0e
--- /dev/null
+++ b/test-suite/bugs/closed/4001.v
@@ -0,0 +1,18 @@
+(* Computing the type constraints to be satisfied when building the
+   return clause of a match with a match *)
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+  
+Variable A : Type.
+Variable typ : A -> Type.
+
+Inductive t : list A -> Type :=
+| snil  : t nil
+| scons : forall (x : A) (e : typ x) (lx : list A) (le : t  lx), t (x::lx).
+
+Definition car (x:A) (lx : list A) (s: t (x::lx)) : typ x :=
+  match s in t l'  with
+  | snil => False
+  | scons _ e _ _ => e
+  end.
diff --git a/test-suite/bugs/closed/4017.v b/test-suite/bugs/closed/4017.v
new file mode 100644
index 0000000000..a6f177b496
--- /dev/null
+++ b/test-suite/bugs/closed/4017.v
@@ -0,0 +1,6 @@
+(* Use of implicit arguments was lost in multiple variable declarations *)
+Variables 
+  (A1 : Type)
+  (A2 : forall (x1 : A1), Type) 
+  (A3 : forall (x1 : A1) (x2 : A2 x1), Type)
+  (A4 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2), Type).
diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v
new file mode 100644
index 0000000000..c3a045943c
--- /dev/null
+++ b/test-suite/bugs/closed/4018.v
@@ -0,0 +1,3 @@
+(* Catching PatternMatchingFailure was lost at some point *)
+Goal nat -> True.
+intros [=].
diff --git a/test-suite/success/TacticNotation1.v b/test-suite/success/TacticNotation1.v
new file mode 100644
index 0000000000..289f2816e5
--- /dev/null
+++ b/test-suite/success/TacticNotation1.v
@@ -0,0 +1,20 @@
+Module Type S.
+End S.
+
+Module F (E : S).
+
+  Tactic Notation "foo" := idtac.
+
+  Ltac bar := foo.
+
+End F.
+
+Module G (E : S).
+  Module M := F E.
+
+  Lemma Foo : True.
+  Proof.
+  M.bar.
+  Abort.
+
+End G.
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index edf7ee8e35..20dd69f826 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -405,7 +405,7 @@ let set_kw =
 
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
-  | "Ltac"
+  | ("Local" space+)? "Ltac"
   | "Require"
   | "Import"
   | "Export"
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 608747d0e4..754ad85261 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -233,9 +233,9 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma
   in
     (gr,inst,Lib.is_modtype_strict ())
 
-let interp_assumption evdref env bl c =
+let interp_assumption evdref env impls bl c =
   let c = prod_constr_expr c bl in
-  let ty, impls = interp_type_evars_impls env evdref c in
+  let ty, impls = interp_type_evars_impls env evdref ~impls c in
   let evd, nf = nf_evars_and_universes !evdref in
   let ctx = Evd.universe_context_set evd in
     ((nf ty, ctx), impls)
@@ -259,12 +259,15 @@ let do_assumptions (_, poly, _ as kind) nl l =
         l []
     else l
   in
-  let _,l = List.fold_map (fun env (is_coe,(idl,c)) ->
-    let (t,ctx),imps = interp_assumption evdref env [] c in
+  let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) ->
+    let (t,ctx),imps = interp_assumption evdref env ienv [] c in
     let env =
       push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in
-      (env,((is_coe,idl),t,(ctx,imps)))) 
-    env l 
+    let ienv = List.fold_right (fun (_,id) ienv ->
+      let impls = compute_internalization_data env Variable t imps in
+      Id.Map.add id impls ienv) idl ienv in
+      ((env,ienv),((is_coe,idl),t,(ctx,imps)))) 
+    (env,empty_internalization_env) l
   in
   let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in
   let l = List.map (on_pi2 (nf_evar evd)) l in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index b3de3a7c7a..0b0fd4ef16 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -61,31 +61,34 @@ let rec make_tags = function
   | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l
   | [] -> []
 
+let make_fresh_key =
+  let id = Summary.ref ~name:"Tactic Notation counter" 0 in
+  fun () -> KerName.make
+    (Safe_typing.current_modpath (Global.safe_env ()))
+    (Global.current_dirpath ())
+    (incr id; Label.make ("_" ^ string_of_int !id))
+
 type tactic_grammar_obj = {
+  tacobj_key : KerName.t;
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
   tacobj_tacpp : Pptactic.pp_tactic;
   tacobj_body : Tacexpr.glob_tactic_expr
 }
 
-let key k tobj =
-  let mp,dp,_ = KerName.repr k in
-  KerName.make mp dp
-    (Label.make ("_" ^ string_of_int (Hashtbl.hash tobj.tacobj_tacgram)))
-
-let cache_tactic_notation ((_,k), tobj) =
-  let key = key k tobj in
+let cache_tactic_notation (_, tobj) =
+  let key = tobj.tacobj_key in
   Tacenv.register_alias key tobj.tacobj_body;
   Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
 
-let open_tactic_notation i ((_,k), tobj) =
-  let key = key k tobj in
+let open_tactic_notation i (_, tobj) =
+  let key = tobj.tacobj_key in
   if Int.equal i 1 && not tobj.tacobj_local then
     Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
 
-let load_tactic_notation i ((_,k), tobj) =
-  let key = key k tobj in
+let load_tactic_notation i (_, tobj) =
+  let key = tobj.tacobj_key in
   (** Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
@@ -93,7 +96,10 @@ let load_tactic_notation i ((_,k), tobj) =
     Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
 
 let subst_tactic_notation (subst, tobj) =
-  { tobj with tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; }
+  { tobj with
+    tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
+    tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body;
+  }
 
 let classify_tactic_notation tacobj = Substitute tacobj
 
@@ -123,6 +129,7 @@ let add_tactic_notation (local,n,prods,e) =
     tacgram_prods = prods;
   } in
   let tacobj = {
+    tacobj_key = make_fresh_key ();
     tacobj_local = local;
     tacobj_tacgram = parule;
     tacobj_tacpp = pprule;